awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
h : finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
⊢ Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0

Tactic:
simp [← finrank_eq_rank, h]

Premises used: Module.finrank_eq_rank
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
⊢ 0 < rankAtStalk M p ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p

Tactic:
Nat.pos_iff_ne_zero.trans (rankAtStalk_eq_zero_iff_notMem_support _).not_left

Premises used: Module.rankAtStalk_eq_zero_iff_notMem_support, Nat.pos_iff_ne_zero, Iff.not_left, Iff.trans
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0 ↔ Subsingleton M

Tactic:
⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩

Premises used: Iff.intro, Module.rankAtStalk_eq_zero_of_subsingleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
refine : ∀ (h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0), Subsingleton M
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0 ↔ Subsingleton M

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
simp_rw : ∀ (x : PrimeSpectrum R), x ∉ support R M
⊢ Subsingleton M

Tactic:
simp_rw [← support_eq_empty_iff (R := R), Set.eq_empty_iff_forall_notMem]

Premises used: Module.support_eq_empty_iff, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
p : PrimeSpectrum R
rw : rankAtStalk M p = 0
rw₁ : Eq (α := ℕ) (0 p) 0
rw₂ rw₃ : Eq (α := ℕ) 0 0
⊢ p ∉ support R M

Tactic:
rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]

Premises used: Module.rankAtStalk_eq_zero_iff_notMem_support, Pi.zero_apply
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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 : Flat R N
inst_8 : Module.Finite R N
h :
  ∀ (p : PrimeSpectrum R),
    rankAtStalk (M × N) p =
      HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M × N) = HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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 : Flat R N
inst_8 : Module.Finite R N
p : PrimeSpectrum R
e : LocalizedModule p.asIdeal.primeCompl (M × N) ≃ₗ[Localization.AtPrime p.asIdeal]
  LocalizedModule p.asIdeal.primeCompl M × LocalizedModule p.asIdeal.primeCompl N :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl (M × N))
      (LinearMap.prodMap (mkLinearMap p.asIdeal.primeCompl M) (mkLinearMap p.asIdeal.primeCompl N)))
⊢ rankAtStalk (M × N) p =
    HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p

Tactic:
simp [rankAtStalk, e.finrank_eq]

Premises used: Module.rankAtStalk, LinearEquiv.finrank_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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)
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)
⊢ rankAtStalk (S ⊗[R] M) p = rankAtStalk M (comap (algebraMap R S) p)

Tactic:
rw [rankAtStalk, e.finrank_eq]

Premises used: Module.rankAtStalk, LinearEquiv.finrank_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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)
⊢ 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:
apply Module.finrank_baseChange

Premises used: Module.finrank_baseChange
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
h :
  ∀ (p : PrimeSpectrum R),
    rankAtStalk (M ⊗[R] N) p =
      HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
⊢ rankAtStalk (M ⊗[R] N) = HMul.hMul (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
h₅ h₆ : rankAtStalk M p * rankAtStalk N p = rankAtStalk M p * rankAtStalk N p
⊢ rankAtStalk (M ⊗[R] 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]

Premises used: Pi.mul_apply, Module.rankAtStalk_eq_finrank_tensorProduct, LinearEquiv.finrank_eq, Module.finrank_tensorProduct
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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
N : Type u_2
inst_7 : AddCommGroup N
inst_8 : Module R N
inst_9 : Module S N
inst_10 : IsScalarTower R S N
inst_11 : Module.Finite S N
inst_12 : Flat S N
p : PrimeSpectrum S
⊢ rankAtStalk (N ⊗[R] M) p = rankAtStalk N p * rankAtStalk M (comap (algebraMap R S) p)

Tactic:
simp [rankAtStalk_eq_of_equiv (AlgebraTensorModule.cancelBaseChange R S S N M).symm,
    rankAtStalk_tensorProduct, rankAtStalk_baseChange]

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, Module.rankAtStalk_baseChange, Module.rankAtStalk_eq_of_equiv, Module.rankAtStalk_tensorProduct
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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)
rw₂ rw₃ :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) =
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
⊢ rankAtStalk M p = finrank p.asIdeal.ResidueField (p.asIdeal.Fiber M)

Tactic:
rw [← e.finrank_eq, finrank_baseChange, rankAtStalk_eq_finrank_tensorProduct]

Premises used: Module.rankAtStalk_eq_finrank_tensorProduct, LinearEquiv.finrank_eq, Module.finrank_baseChange
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
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 : Ideal R
hp : p.IsPrime
⊢ finrank p.ResidueField (p.Fiber M) = rankAtStalk M { asIdeal := p, isPrime := hp : PrimeSpectrum R }

Tactic:
(rankAtStalk_eq ⟨p, hp⟩).symm

Premises used: PrimeSpectrum.mk, Module.rankAtStalk_eq, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
rw : IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : ℕ), {x : PrimeSpectrum R | f.coeff i ∉ x.asIdeal})
⊢ IsOpen (imageOfDf f)

Tactic:
rw [imageOfDf, setOf_exists fun i (x : PrimeSpectrum R) => coeff f i ∉ x.asIdeal]

Premises used: AlgebraicGeometry.Polynomial.imageOfDf, Membership.mem, Set.setOf_exists, Polynomial.coeff, PrimeSpectrum.asIdeal, Not
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : ℕ), {x : PrimeSpectrum R | f.coeff i ∉ x.asIdeal})

Tactic:
isOpen_iUnion fun i => isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen, isOpen_iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
⊢ IsOpen.{u_1} (X := PrimeSpectrum R) (⋃ (i : ℕ), {x : PrimeSpectrum R | f.coeff i ∉ x.asIdeal})

Tactic:
exact isOpen_iUnion fun i => isOpen_basicOpen

Premises used: PrimeSpectrum.isOpen_basicOpen, isOpen_iUnion
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
I : PrimeSpectrum R[X]
H : Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ I
⊢ PrimeSpectrum.comap C I ∈ imageOfDf f

Tactic:
exists_C_coeff_notMem (mem_compl_zeroLocus_iff_notMem.mp H)

Premises used: Set.Mem, setOf, PrimeSpectrum.mem_compl_zeroLocus_iff_notMem, AlgebraicGeometry.Polynomial.imageOfDf, Set.preimage, Iff.mp, exists_C_coeff_notMem
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
h :
  ∀ (x : PrimeSpectrum R),
    x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x
⊢ imageOfDf f = PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
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

Tactic:
⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩

Premises used: Polynomial.C, PrimeSpectrum.mk, Ideal.map, Ideal.isPrime_map_C_of_isPrime, And.intro, Iff.intro, Exists.intro, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
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
h₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x → x ∈ imageOfDf f
⊢ x ∈ imageOfDf f ↔ Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.comap C '' (zeroLocus {f})ᶜ) x

Tactic:
refine ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime⟩, ⟨?_, ?_⟩⟩, ?_⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
h :
  f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])
⊢ Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ
    { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ }

Tactic:
rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, PrimeSpectrum.mem_zeroLocus, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
h :
  ∀ (i : ℕ) (hi : f.coeff i ∉ x.asIdeal),
    f ∉
      (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])
⊢ f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])

Tactic:
obtain ⟨i, hi⟩ := hx
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : f.coeff i ∉ x.asIdeal
⊢ f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])

Tactic:
fun a => hi (mem_map_C_iff.mp a i)

Premises used: Ideal.mem_map_C_iff, Iff.mp, Not
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
i : ℕ
hi : f.coeff i ∉ x.asIdeal
⊢ f ∉ (↑(asIdeal { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ : PrimeSpectrum R[X] }) : Set R[X])

Tactic:
exact fun a => hi (mem_map_C_iff.mp a i)

Premises used: Ideal.mem_map_C_iff, Iff.mp
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x : PrimeSpectrum R
hx : x ∈ imageOfDf f
h :
  ∀ (x_1 : R),
    Membership.mem (γ := Ideal R)
        (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ })) x_1 ↔
      x_1 ∈ x.asIdeal
⊢ PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x.asIdeal, isPrime := ⋯ } = x

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
⊢ Membership.mem (γ := Ideal R)
      (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x ↔
    x ∈ x_1.asIdeal

Tactic:
⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩

Premises used: Polynomial.C, Ideal.subset_span, Set.mem_image_of_mem, Iff.intro, RingHom.toMonoidHom, DFunLike.coe
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
h :
  ∀
    (h :
      Membership.mem (γ := Ideal R)
        (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x),
    x ∈ x_1.asIdeal
⊢ Membership.mem (γ := Ideal R)
      (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x ↔
    x ∈ x_1.asIdeal

Tactic:
refine ⟨fun h => ?_, fun h => subset_span (mem_image_of_mem C.1 h)⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
h :
  Membership.mem (γ := Ideal R)
    (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x
h₁ : coeff ((C : (a : R) → R[X]) x) 0 ∈ x_1.asIdeal
⊢ x ∈ x_1.asIdeal

Tactic:
rw [← @coeff_C_zero R x _]

Premises used: Polynomial.coeff_C_zero
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
h :
  Membership.mem (γ := Ideal R)
    (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x
⊢ coeff ((C : (a : R) → R[X]) x) 0 ∈ x_1.asIdeal

Tactic:
mem_map_C_iff.mp h 0

Premises used: Set.Mem, Ideal.mem_map_C_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
x_1 : PrimeSpectrum R
hx : x_1 ∈ imageOfDf f
x : R
h :
  Membership.mem (γ := Ideal R)
    (asIdeal (PrimeSpectrum.comap C { asIdeal := Ideal.map (F := R →+* R[X]) C x_1.asIdeal, isPrime := ⋯ })) x
⊢ coeff ((C : (a : R) → R[X]) x) 0 ∈ x_1.asIdeal

Tactic:
exact mem_map_C_iff.mp h 0

Premises used: Ideal.mem_map_C_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ xli
⊢ PrimeSpectrum.comap C xli ∈ imageOfDf f

Tactic:
comap_C_mem_imageOfDf complement

Premises used: AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf
-- Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC
Goal:
R : Type u_1
inst : CommRing R
f : R[X]
xli : PrimeSpectrum R[X]
complement : Membership.mem (γ := Set (PrimeSpectrum R[X])) (zeroLocus {f})ᶜ xli
⊢ PrimeSpectrum.comap C xli ∈ imageOfDf f

Tactic:
exact comap_C_mem_imageOfDf complement

Premises used: AlgebraicGeometry.Polynomial.comap_C_mem_imageOfDf