awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f : R_1 →+* S_1
hf : f.FinitePresentation
s : Set (PrimeSpectrum S_1)
hs : IsConstructible s
R : Type u_1
inst_2 : CommRing R
S : Type u_1
refine_2 :
  ∀ [inst : CommRing S] (T : Type u_2) [inst_3 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst_2 S inst f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst T inst_3 g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 T inst_3 (g.comp f)
⊢ ∀ [inst : CommRing S] (T : Type u_2) [inst_3 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst_2 S inst f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst T inst_3 g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 T inst_3 (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f : R_1 →+* S_1
hf : f.FinitePresentation
s : Set (PrimeSpectrum S_1)
hs : IsConstructible s
R : Type u_1
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
T : Type u_2
refine_2 :
  ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst_2 S inst_3 f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst_3 T inst g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 T inst (g.comp f)
⊢ ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_1) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
          ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
        R inst_2 S inst_3 f →
      (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          S inst_3 T inst g →
        (fun (x : Type u_1) (x_1 : CommRing x) (x_2 : Type u_2) (x_3 : CommRing x_2) (f : x →+* x_2) ↦
            ∀ (s : Set (PrimeSpectrum x_2)), IsConstructible s → IsConstructible (comap f '' s))
          R inst_2 T inst (g.comp f)

Tactic:
_
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
T : Type u_2
inst_4 : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
refine_2 : IsConstructible (comap f '' comap g '' s)
⊢ IsConstructible (comap (g.comp f) '' s)

Tactic:
simp only [comap_comp, Set.image_comp]

Premises used: Set.image_comp, PrimeSpectrum.comap_comp
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
T : Type u_2
inst_4 : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
⊢ IsConstructible (comap f '' comap g '' s)

Tactic:
H₁ _ (H₂ _ hs)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R_1 : Type u_1
S_1 : Type u_2
inst : CommRing R_1
inst_1 : CommRing S_1
f_1 : R_1 →+* S_1
hf : f_1.FinitePresentation
s_1 : Set (PrimeSpectrum S_1)
hs_1 : IsConstructible s_1
R : Type u_1
inst_2 : CommRing R
S : Type u_1
inst_3 : CommRing S
T : Type u_2
inst_4 : CommRing T
f : R →+* S
g : S →+* T
H₁ : ∀ (s : Set (PrimeSpectrum S)), IsConstructible s → IsConstructible (comap f '' s)
H₂ : ∀ (s : Set (PrimeSpectrum T)), IsConstructible s → IsConstructible (comap g '' s)
s : Set (PrimeSpectrum T)
hs : IsConstructible s
⊢ IsConstructible (comap f '' comap g '' s)

Tactic:
exact H₁ _ (H₂ _ hs)
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FinitePresentation
⊢ IsConstructible (Set.range (comap f))

Tactic:
Set.image_univ ▸ isConstructible_comap_image hf .univ

Premises used: Set.image_univ, Eq.rec, Topology.IsConstructible.univ, PrimeSpectrum.isConstructible_comap_image
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
inst_4 : Algebra.FinitePresentation R S
rw :
  ∀ s ∈ Set.image (α := TopologicalSpace.Opens (PrimeSpectrum S)) SetLike.coe (Set.range basicOpen),
    IsOpen (X := PrimeSpectrum R) (comap (algebraMap R S) '' s)
⊢ IsOpenMap (X := PrimeSpectrum S) (Y := PrimeSpectrum R) (comap (algebraMap R S))

Tactic:
rw [isBasis_basic_opens.isOpenMap_iff]

Premises used: TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, PrimeSpectrum.isBasis_basic_opens
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
inst_4 : Algebra.FinitePresentation R S
f : S
⊢ IsOpen (X := PrimeSpectrum R) (comap (algebraMap R S) '' (↑(basicOpen f) : Set (PrimeSpectrum S)))

Tactic:
isOpen_of_stableUnderGeneralization_of_isConstructible
    ((basicOpen f).2.stableUnderGeneralization.image
      (Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
    (isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›)
      isConstructible_basicOpen)

Premises used: Iff.mpr, PrimeSpectrum.basicOpen, PrimeSpectrum.isConstructible_basicOpen, PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible, Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, Iff.mp, RingHom.finitePresentation_algebraMap, PrimeSpectrum.isConstructible_comap_image, TopologicalSpace.Opens.is_open', StableUnderGeneralization.image, IsOpen.stableUnderGeneralization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
inst_4 : Algebra.FinitePresentation R S
f : S
⊢ IsOpen (X := PrimeSpectrum R) (comap (algebraMap R S) '' (↑(basicOpen f) : Set (PrimeSpectrum S)))

Tactic:
exact isOpen_of_stableUnderGeneralization_of_isConstructible
    ((basicOpen f).2.stableUnderGeneralization.image
      (Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
    (isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›)
      isConstructible_basicOpen)

Premises used: Iff.mpr, PrimeSpectrum.basicOpen, PrimeSpectrum.isConstructible_basicOpen, PrimeSpectrum.isOpen_of_stableUnderGeneralization_of_isConstructible, Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, Iff.mp, RingHom.finitePresentation_algebraMap, PrimeSpectrum.isConstructible_comap_image, TopologicalSpace.Opens.is_open', StableUnderGeneralization.image, IsOpen.stableUnderGeneralization
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
inr :
  ∀
    (this :
      ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
        (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
        IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U))
    (hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
wlog :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
    (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)

Tactic:
wlog hU' : ∃ f, U = SetLike.coe (basicOpen f) generalizing U
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
    (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
inr :
  IsOpen.{u_4} (X := PrimeSpectrum A)
    (⋃ (i : A ⊗[K] B),
      ⋃ (_ : (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))) ⊆ U),
        comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)

Tactic:
rw [eq_biUnion_of_isOpen hU, Set.image_iUnion₂]

Premises used: PrimeSpectrum.eq_biUnion_of_isOpen, Set.image_iUnion₂
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
    (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen.{u_4} (X := PrimeSpectrum A)
    (⋃ (i : A ⊗[K] B),
      ⋃ (_ : (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))) ⊆ U),
        comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))))

Tactic:
isOpen_iUnion fun _ ↦ isOpen_iUnion fun _ ↦ this _ (basicOpen _).isOpen ⟨_, rfl⟩

Premises used: PrimeSpectrum.basicOpen, SetLike.coe, isOpen_iUnion, TopologicalSpace.Opens.isOpen, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
this :
  ∀ (U : Set (PrimeSpectrum (A ⊗[K] B))) (hU : IsOpen U)
    (hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)
hU' : ¬∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
⊢ IsOpen.{u_4} (X := PrimeSpectrum A)
    (⋃ (i : A ⊗[K] B),
      ⋃ (_ : (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))) ⊆ U),
        comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen i) : Set (PrimeSpectrum (A ⊗[K] B))))

Tactic:
exact isOpen_iUnion fun _ ↦ isOpen_iUnion fun _ ↦ this _ (basicOpen _).isOpen ⟨_, rfl⟩

Premises used: PrimeSpectrum.basicOpen, SetLike.coe, isOpen_iUnion, TopologicalSpace.Opens.isOpen, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
U : Set (PrimeSpectrum (A ⊗[K] B))
hU : IsOpen U
hU' : ∃ (f : A ⊗[K] B), U = (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
obtain :
  ∀ (f : A ⊗[K] B) (hU : IsOpen (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B))))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' U)

Tactic:
obtain ⟨f, rfl⟩ := hU'

Premises used: rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
f : A ⊗[K] B
hU : IsOpen (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B)))
obtain :
  ∀ (B' : Subalgebra K B) (hB : B'.FG) (f : TensorProduct.{u_3, u_4, u_5} K A ↥B')
    (hU :
      IsOpen
        (↑(basicOpen
                ((AlgHom.toRingHom
                      (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                        TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                    (a : A ⊗[K] ↥B') → A ⊗[K] B)
                  f) :
              TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
          Set (PrimeSpectrum (A ⊗[K] B)))),
    IsOpen (X := PrimeSpectrum A)
      (comap (algebraMap A (A ⊗[K] B)) ''
        (↑(basicOpen
                ((AlgHom.toRingHom
                      (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                        TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                    (a : A ⊗[K] ↥B') → A ⊗[K] B)
                  f) :
              TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
          Set (PrimeSpectrum (A ⊗[K] B))))
⊢ IsOpen (X := PrimeSpectrum A) (comap (algebraMap A (A ⊗[K] B)) '' (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] B))))

Tactic:
obtain ⟨B', hB, f, rfl⟩ := exists_fg_and_mem_baseChange f

Premises used: exists_fg_and_mem_baseChange, rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
⊢ Algebra.FinitePresentation.{u_3, u_5} K ↥B'

Tactic:
have : Algebra.FinitePresentation K B' :=
    Algebra.FinitePresentation.of_finiteType.mp ⟨B'.fg_top.mpr hB⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
⊢ IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
      (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))

Tactic:
isOpenMap_comap_of_hasGoingDown_of_finitePresentation (R := A) (S := A ⊗[K] B') _
      (basicOpen f).isOpen

Premises used: PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation, PrimeSpectrum.basicOpen, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
h :
  Eq (α := Set (PrimeSpectrum A))
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
    (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
      (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
⊢ IsOpen (X := PrimeSpectrum A)
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))

Tactic:
convert!
    isOpenMap_comap_of_hasGoingDown_of_finitePresentation (R := A) (S := A ⊗[K] B') _
      (basicOpen f).isOpen using 1

Premises used: PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation, PrimeSpectrum.basicOpen, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
h :
  ∀ (x : PrimeSpectrum A),
    Membership.mem (γ := Set (PrimeSpectrum A))
        (comap (algebraMap A (A ⊗[K] B)) ''
          (↑(basicOpen
                  ((AlgHom.toRingHom
                        (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                          TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                      (a : A ⊗[K] ↥B') → A ⊗[K] B)
                    f) :
                TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
            Set (PrimeSpectrum (A ⊗[K] B))))
        x ↔
      Membership.mem (γ := Set (PrimeSpectrum A))
        (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
          (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
        x
⊢ Eq (α := Set (PrimeSpectrum A))
    (comap (algebraMap A (A ⊗[K] B)) ''
      (↑(basicOpen
              ((AlgHom.toRingHom
                    (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                      TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                  (a : A ⊗[K] ↥B') → A ⊗[K] B)
                f) :
            TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
        Set (PrimeSpectrum (A ⊗[K] B))))
    (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
      (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley
Goal:
K : Type u_3
A : Type u_4
B : Type u_5
inst : Field K
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra K A
inst_4 : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : TensorProduct.{u_3, u_4, u_5} K A ↥B'
hU :
  IsOpen
    (↑(basicOpen
            ((AlgHom.toRingHom
                  (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                    TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                (a : A ⊗[K] ↥B') → A ⊗[K] B)
              f) :
          TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
      Set (PrimeSpectrum (A ⊗[K] B)))
this : Algebra.FinitePresentation.{u_3, u_5} K ↥B'
x : PrimeSpectrum A
h :
  IsNilpotent (R := A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
      ((algebraMap (A ⊗[K] B) (A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) :
            (a : A ⊗[K] B) → A ⊗[K] B ⊗[A] x.asIdeal.ResidueField)
          ((AlgHom.toRingHom
                (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                  TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
              (a : A ⊗[K] ↥B') → A ⊗[K] B)
            f) :
        A ⊗[K] B ⊗[A] x.asIdeal.ResidueField) ↔
    IsNilpotent (R := TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
      ((algebraMap (TensorProduct.{u_3, u_4, u_5} K A ↥B')
              (TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField) :
            (a : A ⊗[K] ↥B') → A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField)
          f :
        TensorProduct.{u_3, u_4, u_5} K A ↥B' ⊗[A] x.asIdeal.ResidueField)
⊢ Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (A ⊗[K] B)) ''
        (↑(basicOpen
                ((AlgHom.toRingHom
                      (Algebra.TensorProduct.map (AlgHom.id A A) B'.val :
                        TensorProduct.{u_3, u_4, u_5} K A ↥B' →ₐ[A] A ⊗[K] B) :
                    (a : A ⊗[K] ↥B') → A ⊗[K] B)
                  f) :
              TopologicalSpace.Opens (PrimeSpectrum (A ⊗[K] B))) :
          Set (PrimeSpectrum (A ⊗[K] B))))
      x ↔
    Membership.mem (γ := Set (PrimeSpectrum A))
      (comap (algebraMap A (TensorProduct.{u_3, u_4, u_5} K A ↥B')) ''
        (↑(basicOpen f) : Set (PrimeSpectrum (A ⊗[K] ↥B'))))
      x

Tactic:
rw [PrimeSpectrum.mem_image_comap_basicOpen, PrimeSpectrum.mem_image_comap_basicOpen,
    not_iff_not]

Premises used: not_iff_not, PrimeSpectrum.mem_image_comap_basicOpen
-- Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
Goal:
R₀ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R₀
inst_1 : CommRing R
inst_2 : Algebra R₀ R
inst_3 : CommRing S
inst_4 : Algebra R₀ S
n : ℕ
e : InductionObj R n
f : R →ₐ[R₀] S
⊢ coeffSubmodule R₀ { val := (⇑(mapRingHom (↑f : R →+* S)) : (a : R[X]) → S[X]) ∘ e.val : InductionObj S n } =
    Submodule.map f.toLinearMap (coeffSubmodule R₀ e)

Tactic:
simp [coeffSubmodule, Submodule.map_span, Set.image_insert_eq, Set.image_iUnion, ← Set.range_comp,
    coeff_map_eq_comp]

Premises used: Set.range_comp, Polynomial.coeff_map_eq_comp, Set.image_iUnion, Set.image_insert_eq, Submodule.map_span, _private.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule