-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma isOpenMap_over : IsOpenMap (𝔸(n; S) ↘ S).base

Proof state:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ ∀ (i : S.affineCover.1), topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
intro i

Result:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.1
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Proof state:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically (@IsOpenMap) (𝔸(n; Spec R) ↘ Spec R)

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
  (SpecIso n R).inv, SpecIso_inv_over]

Result:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically (@IsOpenMap) (Spec.map (CommRingCat.ofHom C))

Proof state:
n : Type v
S : Scheme
⊢ IsOpenMap ⇑(ConcreteCategory.hom (𝔸(n; S) ↘ S).base)

Tactic:
show topologically @IsOpenMap _

Result:
n : Type v
S : Scheme
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Proof state:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically (@IsOpenMap) (Spec.map (CommRingCat.ofHom C))

Tactic:
exact MvPolynomial.isOpenMap_comap_C

Result:
no goals

Proof state:
case inr
n : Type v
S : Scheme
this✝ : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.1
this : topologically (@IsOpenMap) (𝔸(n; S.affineCover.obj i) ↘ S.affineCover.obj i)
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
rwa [← (isPullback_map (n := n)  (S.affineCover.map i)).isoPullback_hom_snd,
  MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this

Result:
no goals

Proof state:
n✝ : Type v
S✝ : Scheme
n : Type v
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
obtain ⟨R, rfl⟩ := hS

Result:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
⊢ topologically (@IsOpenMap) (𝔸(n; Spec R) ↘ Spec R)

Proof state:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
refine (IsLocalAtTarget.iff_of_openCover (P := topologically @IsOpenMap) S.affineCover).mpr ?_

Result:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ ∀ (i : S.affineCover.1), topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Proof state:
n : Type v
S : Scheme
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Tactic:
wlog hS : ∃ R, S = Spec R

Result:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

n✝ : Type v
S✝ : Scheme
n : Type v
S : Scheme
hS : ∃ R, S = Spec R
⊢ topologically (@IsOpenMap) (𝔸(n; S) ↘ S)

Proof state:
case inr
n : Type v
S : Scheme
this : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.1
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)

Tactic:
have := this (n := n) (S.affineCover.obj i) ⟨_, rfl⟩

Result:
case inr
n : Type v
S : Scheme
this✝ : ∀ {n : Type v} (S : Scheme), (∃ R, S = Spec R) → topologically (@IsOpenMap) (𝔸(n; S) ↘ S)
hS : ¬∃ R, S = Spec R
i : S.affineCover.1
this : topologically (@IsOpenMap) (𝔸(n; S.affineCover.obj i) ↘ S.affineCover.obj i)
⊢ topologically (@IsOpenMap) (Scheme.Cover.pullbackHom S.affineCover (𝔸(n; S) ↘ S) i)