awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx :
  Membership.mem (α := P.infinitesimal.Ring) (γ := Ideal P.infinitesimal.Ring) ⊥
    ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)
⊢ (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
        Ideal.Quotient.eq_zero_iff_mem] using hx

Premises used: Ideal.mem_bot, Ideal.Quotient.eq_zero_iff_mem, Algebra.Extension.toInfinitesimal, Algebra.Extension.infinitesimal
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx :
  Eq (α := P.infinitesimal.Cotangent)
    ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x) :
      P.infinitesimal.Cotangent)
    (0 : P.infinitesimal.Cotangent)
⊢ (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2

Tactic:
have hx : x.1 ∈ P.ker ^ 2 := by
      apply_fun Cotangent.val at hx
      simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
        Extension.ker_infinitesimal] at hx
      rw [Ideal.cotangentIdeal_square] at hx
      simpa only [toInfinitesimal, Ideal.mem_bot, infinitesimal,
        Ideal.Quotient.eq_zero_iff_mem] using hx
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : ↥P.ker
hx_1 :
  Eq (α := P.infinitesimal.Cotangent)
    ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x) :
      P.infinitesimal.Cotangent)
    (0 : P.infinitesimal.Cotangent)
hx : (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
⊢ Eq.{u + 1} (α := P.ker.Cotangent) (val ((mk : (a : ↥P.ker) → P.Cotangent) x)) (val 0)

Tactic:
simpa [Ideal.toCotangent_eq_zero]

Premises used: Ideal.toCotangent_eq_zero
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.infinitesimal.Cotangent
right :
  ∀ (x : P.infinitesimal.Ring) (hx : x ∈ P.infinitesimal.ker),
    ∃ (a : P.Cotangent),
      Eq (α := P.infinitesimal.Cotangent)
        ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
        ((mk : (a : ↥P.infinitesimal.ker) → P.infinitesimal.Cotangent)
            (Subtype.mk (p := fun (x : P.infinitesimal.Ring) ↦ x ∈ P.infinitesimal.ker) x hx) :
          P.infinitesimal.Cotangent)
⊢ ∃ (a : P.Cotangent), (map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a = x

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := Cotangent.mk_surjective x

Premises used: Algebra.Extension.Cotangent.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.infinitesimal.Ring
hx : x ∈ P.infinitesimal.ker
right :
  ∀ (x : P.Ring)
    (hx :
      Membership.mem (α := P.infinitesimal.Ring) P.infinitesimal.ker
        ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x :
          P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)),
    ∃ (a : P.Cotangent),
      Eq (α := P.infinitesimal.Cotangent)
        ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
        ((mk : (a : ↥P.infinitesimal.ker) → P.infinitesimal.Cotangent)
            (Subtype.mk (p := fun (x : P.infinitesimal.Ring) ↦ x ∈ P.infinitesimal.ker)
              ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x) hx) :
          P.infinitesimal.Cotangent)
⊢ ∃ (a : P.Cotangent),
    Eq (α := P.infinitesimal.Cotangent)
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
      ((mk : (a : ↥P.infinitesimal.ker) → P.infinitesimal.Cotangent)
          (Subtype.mk (p := fun (x : P.infinitesimal.Ring) ↦ x ∈ P.infinitesimal.ker) x hx) :
        P.infinitesimal.Cotangent)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Ring
hx :
  Membership.mem (α := P.infinitesimal.Ring) P.infinitesimal.ker
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
⊢ x ∈ P.ker

Tactic:
rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx

Premises used: Ideal.mk_mem_cotangentIdeal, Algebra.Extension.ker_infinitesimal
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Ring
hx_1 :
  Membership.mem (α := P.infinitesimal.Ring) P.infinitesimal.ker
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
hx : x ∈ P.ker
⊢ ∃ (a : P.Cotangent),
    Eq (α := P.infinitesimal.Cotangent)
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
      ((mk : (a : ↥P.infinitesimal.ker) → P.infinitesimal.Cotangent)
          (Subtype.mk (p := fun (x : P.infinitesimal.Ring) ↦ x ∈ P.infinitesimal.ker)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x) hx_1) :
        P.infinitesimal.Cotangent)

Tactic:
⟨.mk ⟨x, hx⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, Algebra.Extension.Cotangent.mk, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Ring
hx_1 :
  Membership.mem (α := P.infinitesimal.Ring) P.infinitesimal.ker
    ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x :
      P.Ring ⧸ HPow.hPow (β := ℕ) P.ker 2)
hx : x ∈ P.ker
⊢ ∃ (a : P.Cotangent),
    Eq (α := P.infinitesimal.Cotangent)
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
      ((mk : (a : ↥P.infinitesimal.ker) → P.infinitesimal.Cotangent)
          (Subtype.mk (p := fun (x : P.infinitesimal.Ring) ↦ x ∈ P.infinitesimal.ker)
            ((Ideal.Quotient.mk (HPow.hPow (β := ℕ) P.ker 2) : (a : P.Ring) → P.Ring ⧸ P.ker ^ 2) x) hx_1) :
        P.infinitesimal.Cotangent)

Tactic:
exact ⟨.mk ⟨x, hx⟩, rfl⟩
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
left :
  Function.Injective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
right :
  Surjective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
⊢ Function.Bijective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x y : P.H1Cotangent
e :
  Eq (α := P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) x : P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) y : P.infinitesimal.H1Cotangent)
left : (↑x : P.Cotangent) = (↑y : P.Cotangent)
⊢ x = y

Tactic:
ext1
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x y : P.H1Cotangent
e :
  Eq (α := P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) x : P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) y : P.infinitesimal.H1Cotangent)
⊢ (↑x : P.Cotangent) = (↑y : P.Cotangent)

Tactic:
(Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)

Premises used: congr_arg, Algebra.Extension.Cotangent.map_toInfinitesimal_bijective, And.left, Subtype.val
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x y : P.H1Cotangent
e :
  Eq (α := P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) x : P.infinitesimal.H1Cotangent)
    ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) y : P.infinitesimal.H1Cotangent)
⊢ (↑x : P.Cotangent) = (↑y : P.Cotangent)

Tactic:
exact (Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)

Premises used: congr_arg, Algebra.Extension.Cotangent.map_toInfinitesimal_bijective, And.left, Subtype.val
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.infinitesimal.Cotangent
hx : x ∈ P.infinitesimal.cotangentComplex.ker
right :
  ∀ (x : P.Cotangent)
    (hx :
      Membership.mem (α := P.infinitesimal.Cotangent) P.infinitesimal.cotangentComplex.ker
        ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x :
          P.infinitesimal.Cotangent)),
    ∃ (a : P.H1Cotangent),
      Eq (α := P.infinitesimal.H1Cotangent)
        ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) a : P.infinitesimal.H1Cotangent)
        (Subtype.mk (p := fun (x : P.infinitesimal.Cotangent) ↦ x ∈ P.infinitesimal.cotangentComplex.ker)
            ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x) hx :
          ↥P.infinitesimal.cotangentComplex.ker)
⊢ ∃ (a : P.H1Cotangent),
    (map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) a =
      Subtype.mk (p := fun (x : P.infinitesimal.Cotangent) ↦ x ∈ P.infinitesimal.cotangentComplex.ker) x hx

Tactic:
obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x

Premises used: Algebra.Extension.Cotangent.map_toInfinitesimal_bijective, And.right, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Cotangent
hx :
  Membership.mem (α := P.infinitesimal.Cotangent) P.infinitesimal.cotangentComplex.ker
    ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x : P.infinitesimal.Cotangent)
⊢ ∃ (a : P.H1Cotangent),
    Eq (α := P.infinitesimal.H1Cotangent)
      ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) a : P.infinitesimal.H1Cotangent)
      (Subtype.mk (p := fun (x : P.infinitesimal.Cotangent) ↦ x ∈ P.infinitesimal.cotangentComplex.ker)
          ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x) hx :
        ↥P.infinitesimal.cotangentComplex.ker)

Tactic:
⟨⟨x, ?_⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Cotangent
hx :
  Membership.mem (α := P.infinitesimal.Cotangent) P.infinitesimal.cotangentComplex.ker
    ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x : P.infinitesimal.Cotangent)
right : x ∈ P.cotangentComplex.ker
⊢ ∃ (a : P.H1Cotangent),
    Eq (α := P.infinitesimal.H1Cotangent)
      ((map P.toInfinitesimal : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent) a : P.infinitesimal.H1Cotangent)
      (Subtype.mk (p := fun (x : P.infinitesimal.Cotangent) ↦ x ∈ P.infinitesimal.cotangentComplex.ker)
          ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x) hx :
        ↥P.infinitesimal.cotangentComplex.ker)

Tactic:
refine ⟨⟨x, ?_⟩, rfl⟩
-- Module: Mathlib.RingTheory.Smooth.Kaehler
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : Extension.{u, u_1, u_3} R S
x : P.Cotangent
hx :
  Membership.mem (α := P.infinitesimal.Cotangent) P.infinitesimal.cotangentComplex.ker
    ((Cotangent.map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x : P.infinitesimal.Cotangent)
⊢ x ∈ P.cotangentComplex.ker

Tactic:
simpa [← CotangentSpace.map_cotangentComplex,
      map_eq_zero_iff _ (CotangentSpace.map_toInfinitesimal_bijective P).injective] using hx

Premises used: Algebra.Extension.CotangentSpace.map_toInfinitesimal_bijective, Algebra.Extension.CotangentSpace.map_cotangentComplex, Function.Bijective.injective, map_eq_zero_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
asIdeal : ∀ (x : S), x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
⊢ q = q'

Tactic:
ext x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
asIdeal : ∀ (n : ℕ) (hn : n > 0) (y : R) (hy : (f : (a : R) → S) y = x ^ n), x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal

Tactic:
obtain ⟨n, hn, y, hy⟩ := H x
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : (f : (a : R) → S) y = x ^ n
asIdeal :
  Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
    Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal

Tactic:
rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]

Premises used: Ideal.IsPrime.pow_mem_iff_mem, PrimeSpectrum.isPrime
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : (f : (a : R) → S) y = x ^ n
asIdeal :
  ∀ (hqq' : ∀ (x : R), x ∈ (comap f q).asIdeal ↔ x ∈ (comap f q').asIdeal) (x : S) (n : ℕ) (hn : n > 0) (y : R)
    (hy : (f : (a : R) → S) y = x ^ n),
    Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
      Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)
⊢ Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
    Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)

Tactic:
rw [PrimeSpectrum.ext_iff, SetLike.ext_iff] at hqq'

Premises used: SetLike.ext_iff, PrimeSpectrum.ext_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
q q' : PrimeSpectrum S
hqq' : ∀ (x : R), x ∈ (comap f q).asIdeal ↔ x ∈ (comap f q').asIdeal
x : S
n : ℕ
hn : n > 0
y : R
hy : (f : (a : R) → S) y = x ^ n
⊢ Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
    Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)

Tactic:
apply hqq'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
⊢ Function.Injective (comap f)

Tactic:
have h1 : Function.Injective (comap f) := by
    intro q q' hqq'
    ext x
    obtain ⟨n, hn, y, hy⟩ := H x
    rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]
    rw [PrimeSpectrum.ext_iff, SetLike.ext_iff] at hqq'
    apply hqq'
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
⊢ f.kerLift.IsIntegral

Tactic:
have hint : f.kerLift.IsIntegral := fun x ↦
    have ⟨n, hn, y, hy⟩ := H x
    let _ := f.kerLift.toAlgebra
    IsIntegral.of_pow hn (hy ▸ f.kerLift.isIntegralElem_map (x := ⟦y⟧))
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
⊢ Function.Bijective (comap f)

Tactic:
have hbij : Function.Bijective (comap f) :=
    ⟨h1, (comap_quotientMk_bijective_of_le_nilradical hker).2.comp <|
      hint.comap_surjective f.kerLift_injective⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
⊢ IsHomeomorph (comap f)

Tactic:
⟨continuous_comap f, ?_, h1, hbij.2⟩

Premises used: IsHomeomorph.mk, PrimeSpectrum.continuous_comap, And.right, And.intro
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
refine : IsOpenMap (comap f)
⊢ IsHomeomorph (comap f)

Tactic:
refine ⟨continuous_comap f, ?_, h1, hbij.2⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
rw :
  ∀ (s : Set (PrimeSpectrum S)),
    Membership.mem (γ := Set (Set (PrimeSpectrum S))) (Set.range fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S)))
        s →
      IsOpen (comap f '' s)
⊢ IsOpenMap (comap f)

Tactic:
rw [isTopologicalBasis_basic_opens.isOpenMap_iff]

Premises used: TopologicalSpace.IsTopologicalBasis.isOpenMap_iff, PrimeSpectrum.isTopologicalBasis_basic_opens
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
obtain :
  ∀ (n : ℕ) (hn : n > 0) (r : R) (hr : (f : (a : R) → S) r = s ^ n),
    IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)
⊢ IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)

Tactic:
obtain ⟨n, hn, r, hr⟩ := H s
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
rw :
  (↑(basicOpen ((f : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S)) : Set (PrimeSpectrum S)) =
    comap f ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ (↑(basicOpen s) : Set (PrimeSpectrum S)) = comap f ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
rw [← basicOpen_pow _ n hn, ← hr]

Premises used: PrimeSpectrum.basicOpen_pow
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
⊢ (↑(basicOpen ((f : (a : R) → S) r) : TopologicalSpace.Opens (PrimeSpectrum S)) : Set (PrimeSpectrum S)) =
    comap f ⁻¹' (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
⊢ comap f '' (↑(basicOpen s) : Set (PrimeSpectrum S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))

Tactic:
have : (comap f) '' (basicOpen s) = basicOpen r :=
    (Set.eq_preimage_iff_image_eq hbij).mp <| by rw [← basicOpen_pow _ n hn, ← hr]; rfl
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
this : comap f '' (↑(basicOpen s) : Set (PrimeSpectrum S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)

Tactic:
this ▸ isOpen_basicOpen

Premises used: Eq.rec, PrimeSpectrum.isOpen_basicOpen, Eq.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, Membership.mem (γ := Subring S) (RingHom.range.{u_3, u_4} (R := R) f) (x ^ n)
hker : LE.le (α := Ideal R) (RingHom.ker f) (nilradical R)
h1 : Function.Injective (comap f)
hint : f.kerLift.IsIntegral
hbij : Function.Bijective (comap f)
s : S
n : ℕ
hn : n > 0
r : R
hr : (f : (a : R) → S) r = s ^ n
this : comap f '' (↑(basicOpen s) : Set (PrimeSpectrum S)) = (↑(basicOpen r) : Set (PrimeSpectrum R))
⊢ IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)

Tactic:
exact this ▸ isOpen_basicOpen