awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
⊢ CotangentSpace.map P.toInfinitesimal =
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R])
have a : Eq (α := LinearMap (R := P.Ring) (RingHom.id P.Ring) P.CotangentSpace P.infinitesimal.CotangentSpace)
  ((↑P.Ring :
      {S_1 : Type u_3} →
        {M M₂ : Type (max u u_3)} →
          [inst_3 : Semiring P.Ring] →
            [inst_4 : Semiring S_1] →
              [inst_5 : AddCommMonoid M] →
                [inst_6 : AddCommMonoid M₂] →
                  [inst_7 : Module P.Ring M] →
                    [inst_8 : Module P.Ring M₂] →
                      [inst_9 : Module S_1 M] →
                        [inst_10 : Module S_1 M₂] →
                          [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
    (CotangentSpace.map P.toInfinitesimal))
  ((↑P.Ring :
      {S_1 : Type u_3} →
        {M M₂ : Type (max u u_3)} →
          [inst_3 : Semiring P.Ring] →
            [inst_4 : Semiring S_1] →
              [inst_5 : AddCommMonoid M] →
                [inst_6 : AddCommMonoid M₂] →
                  [inst_7 : Module P.Ring M] →
                    [inst_8 : Module P.Ring M₂] →
                      [inst_9 : Module S_1 M] →
                        [inst_10 : Module S_1 M₂] →
                          [LinearMap.CompatibleSMul M M₂ P.Ring S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[P.Ring] M₂)
    (↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
      S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
        S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]))
Tactic: apply LinearMap.restrictScalars_injective P.Ring
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
this_1 : Algebra P.Ring P.infinitesimal.Ring :=
  { smul := map_toInfinitesimal_bijective._aux_1 P, algebraMap := map_toInfinitesimal_bijective._aux_2 P,
    commutes' := ⋯, smul_def' := ⋯ }
this : IsScalarTower.{u, u, u_3} P.Ring P.infinitesimal.Ring S
x : S
a : P.Ring
⊢ Eq (α := P.infinitesimal.CotangentSpace)
    ((CotangentSpace.map P.toInfinitesimal : (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)
    (((↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
            S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
              S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
          (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
        (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
      P.infinitesimal.CotangentSpace)
have a₁ : Eq (α := P.infinitesimal.CotangentSpace)
  (x ⊗ₜ[P.infinitesimal.Ring]
      (D R P.infinitesimal.Ring : (a : P.infinitesimal.Ring) → Ω[P.infinitesimal.Ring⁄R])
        ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) a) :
    TensorProduct.{u, u_3, u} P.infinitesimal.Ring S Ω[P.infinitesimal.Ring⁄R])
  (((↑(LinearEquiv.symm (tensorKaehlerQuotKerSqEquiv R P.Ring S)) :
          S ⊗[P.Ring] Ω[P.Ring⁄R] →ₗ[S]
            S ⊗[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2] Ω[P.Ring ⧸ RingHom.ker (algebraMap P.Ring S) ^ 2⁄R]) :
        (a : S ⊗[P.Ring] Ω[P.Ring⁄R]) → P.infinitesimal.CotangentSpace)
      (x ⊗ₜ[P.Ring] (D R P.Ring : (a : P.Ring) → Ω[P.Ring⁄R]) a) :
    P.infinitesimal.CotangentSpace)
Tactic: simp only [map_tmul, algebraMap_self, RingHom.id_apply, Hom.toAlgHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ Function.Bijective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
have left : Function.Injective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
  (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
⊢ Function.Bijective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
have right : Surjective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
  (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ Function.Injective (α := P.Cotangent) (β := P.infinitesimal.Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.Cotangent) → P.infinitesimal.Cotangent)
have left : ∀ (a : P.Cotangent),
  Eq (α := P.infinitesimal.Cotangent)
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a : P.infinitesimal.Cotangent)
      (0 : P.infinitesimal.Cotangent) →
    a = 0
Tactic: rw [injective_iff_map_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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 :
  Eq (α := P.infinitesimal.Cotangent)
    ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) x : P.infinitesimal.Cotangent)
    (0 : P.infinitesimal.Cotangent)
⊢ x = 0
have left : ∀ (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)),
  Eq (α := P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent) (0 : P.Cotangent)
Tactic: obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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
have hx₁ : Eq.{u + 1} (α := P.infinitesimal.ker.Cotangent)
  (val ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
  (val 0)
Tactic: apply_fun Cotangent.val at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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.{u + 1} (α := P.infinitesimal.ker.Cotangent)
    (val
      ((map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x)))
    (val 0)
⊢ (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
have hx₁ : Membership.mem (α := P.infinitesimal.Ring) (HPow.hPow (β := ℕ) P.ker.cotangentIdeal 2)
  ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)
Tactic: simp only [map_mk, Hom.toAlgHom_apply, val_mk, val_zero, Ideal.toCotangent_eq_zero,
        Extension.ker_infinitesimal] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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) (HPow.hPow (β := ℕ) P.ker.cotangentIdeal 2)
    ((P.toInfinitesimal.toRingHom : (a : P.Ring) → P.infinitesimal.Ring) (↑x : P.Ring) : P.infinitesimal.Ring)
⊢ (↑x : P.Ring) ∈ HPow.hPow (β := ℕ) P.ker 2
have 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)
Tactic: rw [Ideal.cotangentIdeal_square] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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)
⊢ Eq (α := P.Cotangent) ((mk : (a : ↥P.ker) → P.Cotangent) x : P.Cotangent) (0 : P.Cotangent)
have hx₁ : (↑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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ ∃ (a : P.Cotangent), (map P.toInfinitesimal : (a : P.Cotangent) → P.infinitesimal.Cotangent) a = x
have 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)
Tactic: obtain ⟨⟨x, hx⟩, rfl⟩ := Cotangent.mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (hypothesis)
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)
⊢ ∃ (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)
have hx₁ : x ∈ P.ker
Tactic: rw [ker_infinitesimal, Ideal.mk_mem_cotangentIdeal] at hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ Function.Bijective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
have left : Function.Injective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
  (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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)
⊢ Function.Bijective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
    (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
have right : Surjective (α := P.H1Cotangent) (β := P.infinitesimal.H1Cotangent)
  (⇑(map P.toInfinitesimal) : (a : P.H1Cotangent) → P.infinitesimal.H1Cotangent)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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 = y
have left : (↑x : P.Cotangent) = (↑y : P.Cotangent)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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
⊢ ∃ (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
have 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)
Tactic: obtain ⟨x, rfl⟩ := (Cotangent.map_toInfinitesimal_bijective P).2 x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Kaehler (goal)
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)
have right : x ∈ P.cotangentComplex.ker
Tactic: refine ⟨⟨x, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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'
⊢ q = q'
have asIdeal : ∀ (x : S), x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
have asIdeal : ∀ (n : ℕ) (hn : n > 0) (y : R) (hy : (f : (a : R) → S) y = x ^ n), x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
Tactic: obtain ⟨n, hn, y, hy⟩ := H x
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
have asIdeal : Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
  Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)
Tactic: rw [← q.2.pow_mem_iff_mem _ hn, ← q'.2.pow_mem_iff_mem _ hn, ← hy]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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
⊢ Membership.mem (α := S) q.asIdeal ((f : (a : R) → S) y : S) ↔
    Membership.mem (α := S) q'.asIdeal ((f : (a : R) → S) y : S)
have 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)
Tactic: rw [PrimeSpectrum.ext_iff, SetLike.ext_iff] at hqq'
Cleared hypotheses: hqq', x, n, hn, y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (hypothesis)
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)
⊢ IsHomeomorph (comap f)
have h1 : 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'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (hypothesis)
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)
⊢ IsHomeomorph (comap f)
have hint : 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⟧))
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (hypothesis)
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
⊢ IsHomeomorph (comap f)
have hbij : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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)
have refine : IsOpenMap (comap f)
Tactic: refine ⟨continuous_comap f, ?_, h1, hbij.2⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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)
⊢ IsOpenMap (comap f)
have 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)
Tactic: rw [isTopologicalBasis_basic_opens.isOpenMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.Homeomorph (goal)
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
⊢ IsOpen (comap f '' (fun (r : S) ↦ (↑(basicOpen r) : Set (PrimeSpectrum S))) s)
have 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)
Tactic: obtain ⟨n, hn, r, hr⟩ := H s