-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma isOpenMap_comap_C : IsOpenMap (comap (R := R) (C (σ := σ)))

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
U : Set (PrimeSpectrum (MvPolynomial σ R))
hU : IsOpen U
⊢ IsOpen (⇑(comap C) '' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := isTopologicalBasis_basic_opens.open_eq_sUnion hU

Result:
case intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⇑(comap C) '' ⋃₀ S)

Proof state:
case intro.intro.h.intro.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun r => ↑(basicOpen r)) r ∈ S
⊢ IsOpen (⇑(comap C) '' (fun r => ↑(basicOpen r)) r)

Tactic:
simp only [image_comap_C_basicOpen]

Result:
case intro.intro.h.intro.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun r => ↑(basicOpen r)) r ∈ S
⊢ IsOpen (zeroLocus (Set.range fun m => coeff m r))ᶜ

Proof state:
case intro.intro.h.intro.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun r => ↑(basicOpen r)) r ∈ S
⊢ IsOpen (zeroLocus (Set.range fun m => coeff m r))ᶜ

Tactic:
exact (isClosed_zeroLocus _).isOpen_compl

Result:
no goals

Proof state:
case intro.intro.h.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum (MvPolynomial σ R))
ht : t ∈ S
⊢ IsOpen (⇑(comap C) '' t)

Tactic:
obtain ⟨r, rfl⟩ := hS ht

Result:
case intro.intro.h.intro.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
r : MvPolynomial σ R
ht : (fun r => ↑(basicOpen r)) r ∈ S
⊢ IsOpen (⇑(comap C) '' (fun r => ↑(basicOpen r)) r)

Proof state:
case intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⇑(comap C) '' ⋃₀ S)

Tactic:
rw [Set.image_sUnion]

Result:
case intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image ⇑(comap C) '' S))

Proof state:
case intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ IsOpen (⋃₀ (Set.image ⇑(comap C) '' S))

Tactic:
apply isOpen_sUnion

Result:
case intro.intro.h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ ∀ t ∈ Set.image ⇑(comap C) '' S, IsOpen t

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ IsOpenMap ⇑(comap C)

Tactic:
intro U hU

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
U : Set (PrimeSpectrum (MvPolynomial σ R))
hU : IsOpen U
⊢ IsOpen (⇑(comap C) '' U)

Proof state:
case intro.intro.h
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
⊢ ∀ t ∈ Set.image ⇑(comap C) '' S, IsOpen t

Tactic:
rintro _ ⟨t, ht, rfl⟩

Result:
case intro.intro.h.intro.intro
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
S : Set (Set (PrimeSpectrum (MvPolynomial σ R)))
hS : S ⊆ Set.range fun r => ↑(basicOpen r)
hU : IsOpen (⋃₀ S)
t : Set (PrimeSpectrum (MvPolynomial σ R))
ht : t ∈ S
⊢ IsOpen (⇑(comap C) '' t)