awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ IsLocalization.Away (f * g) (Localization.Away g₀)
have suffices : IsLocalization.Away (R := Localization.Away f)
  ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f) (Localization.Away g₀)
Tactic: suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ IsLocalization.Away (R := Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
    (Localization.Away g₀)
have refine : g₀ *
    (↑(IsUnit.unit (a :=
          HPow.hPow (α := Localization.Away f) ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) f)
            m)
          sorry) :
      Localization.Away f) =
  (algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g
Tactic: refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
have this₁ : IsLocalization.Away (f * g) (Localization.Away g₀)
Tactic: have : IsLocalization.Away (f * g) (Localization.Away g₀) := by
    suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
    refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
    simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
⊢ IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))
have refine : Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
  (@RingHom.comp _ (MvPolynomial (Fin n) R) _ _ Semiring.toNonAssocSemiring _
    (algebraMap (MvPolynomial (Fin n) R) (Localization.Away (f * g))) (algebraMap R (MvPolynomial (Fin n) R)))
Tactic: refine .of_algebraMap_eq' ?_
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
⊢ Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
    (@RingHom.comp _ (MvPolynomial (Fin n) R) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (MvPolynomial (Fin n) R) (Localization.Away (f * g))) (algebraMap R (MvPolynomial (Fin n) R)))
have simp : Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
  (e.toRingEquiv.toRingHom.comp (algebraMap R (Localization.Away g₀)))
Tactic: simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
⊢ ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
have this₁ : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))
Tactic: have : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g)) := by
    refine .of_algebraMap_eq' ?_
    simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
    exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
⊢ ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
have obtain : ∀ (f : S) (hfp : f ∉ p) (H : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)),
  ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
Tactic: classical
  obtain ⟨f, hfp, H⟩ := IsSmoothAt.exists_notMem_isStandardSmooth R p
  obtain ⟨n, φ, hgC, hg⟩ := RingHom.IsStandardSmooth.exists_etale_mvPolynomial
    (f := algebraMap R (Localization.Away f)) (by simpa [RingHom.isStandardSmooth_algebraMap])
  algebraize [φ]
  have := IsScalarTower.of_algebraMap_eq' hgC.symm
  have : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_›
      ((Ideal.disjoint_powers_iff_notMem_of_isPrime _).mpr hfp)
  obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))
  obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀
  replace hg : g ∉ p := by simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg
  have : IsLocalization.Away (f * g) (Localization.Away g₀) := by
    suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
    refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
    simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]
  let e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
    IsLocalization.algEquiv (.powers (f * g)) _ _
  let : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
    (e.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) _)).toAlgebra
  have : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g)) := by
    refine .of_algebraMap_eq' ?_
    simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
    exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm
  let e' : Localization.Away g₀ ≃ₐ[MvPolynomial (Fin n) R] Localization.Away (f * g) :=
    { __ := e, commutes' r := rfl }
  exact ⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst_7 : P.LiesOver p
inst_8 : p.IsPrime
inst_9 : P.IsPrime
inst_10 : IsUnramifiedAt R p
inst_11 : IsUnramifiedAt A P
this : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
⊢ IsUnramifiedAt R P
have this₁ : FormallyUnramified.{u_3, u_2} (Localization.AtPrime p) (Localization.AtPrime P)
Tactic: have : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P) :=
    .of_restrictScalars A _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal A
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst_7 : Q'.IsPrime
hQ' : Q = Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q'
f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime (R := P.Fiber A) Q' :=
  Localization.localAlgHom Q Q' TensorProduct.includeRight hQ'
⊢ Function.Surjective (α := Localization.AtPrime Q) (β := Localization.AtPrime (R := P.Fiber A) Q')
    (⇑f₀ : (a : Localization.AtPrime Q) → Localization.AtPrime Q')
have subst : ∀
  [inst_8 :
    Ideal.IsPrime (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')]
  [Ideal.LiesOver (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q') P]
  [IsUnramifiedAt R (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')],
  let f₀ :
    Localization.AtPrime
        (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q') →ₐ[R]
      Localization.AtPrime (R := P.Fiber A) Q' :=
    Localization.localAlgHom
      (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q') Q'
      TensorProduct.includeRight sorry;
  Function.Surjective (α :=
    Localization.AtPrime
      (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q'))
    (β := Localization.AtPrime (R := P.Fiber A) Q')
    (⇑f₀ : (a : Localization.AtPrime (Ideal.comap TensorProduct.includeRight.toRingHom Q')) → Localization.AtPrime Q')
Tactic: subst hQ'
Cleared hypotheses: Q, inst_4, inst_5, inst_6, hQ', f₀
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal A
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst_7 : Q'.IsPrime
hQ' : Q = Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q'
f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime (R := P.Fiber A) Q' :=
  Localization.localAlgHom Q Q' TensorProduct.includeRight hQ'
⊢ IsUnramifiedAt P.ResidueField (A := P.Fiber A) Q'
have hf₀ : Function.Surjective (α := Localization.AtPrime Q) (β := Localization.AtPrime (R := P.Fiber A) Q')
  (⇑f₀ : (a : Localization.AtPrime Q) → Localization.AtPrime Q')
Tactic: have hf₀ : Function.Surjective f₀ := by
    subst hQ'; exact P.surjectiveOnStalks_residueField.baseChange' _ _
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
P : Ideal R
inst_3 : P.IsPrime
Q : Ideal A
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
Q' : Ideal (P.Fiber A)
inst_7 : Q'.IsPrime
hQ' : Q = Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q'
f₀ : Localization.AtPrime Q →ₐ[R] Localization.AtPrime (R := P.Fiber A) Q' :=
  Localization.localAlgHom Q Q' TensorProduct.includeRight hQ'
hf₀ :
  Function.Surjective (α := Localization.AtPrime Q) (β := Localization.AtPrime (R := P.Fiber A) Q')
    (⇑f₀ : (a : Localization.AtPrime Q) → Localization.AtPrime Q')
f : Ideal.Fiber.{u_1, u_2} P (Localization.AtPrime Q) →ₐ[P.ResidueField] Localization.AtPrime (R := P.Fiber A) Q' :=
  TensorProduct.lift (ofId P.ResidueField (Localization.AtPrime (R := P.Fiber A) Q')) f₀ ⋯
⊢ IsUnramifiedAt P.ResidueField (A := P.Fiber A) Q'
have hf : Function.Surjective (α := Ideal.Fiber.{u_1, u_2} P (Localization.AtPrime Q)) (β :=
  Localization.AtPrime (R := P.Fiber A) Q') (⇑f : (a : P.Fiber (Localization.AtPrime Q)) → Localization.AtPrime Q')
Tactic: have hf : Function.Surjective f := hf₀.forall.mpr fun x ↦ ⟨1 ⊗ₜ x, by simp [f]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) (Module.support A Ω[A⁄R])ᶜ
have h : ∀ (p : PrimeSpectrum A),
  Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ p
have h : Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
  Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: simp only [Set.mem_compl_iff, Module.notMem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
have h : ∀ (this : LocalizedModule p.asIdeal.primeCompl Ω[A⁄R] ≃ₗ[A] Ω[Localization.AtPrime p.asIdeal⁄R]),
  Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
Tactic: have := IsLocalizedModule.iso p.asIdeal.primeCompl
    (KaehlerDifferential.map R R A (Localization.AtPrime p.asIdeal))
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
f : A
⊢ (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum A)) ⊆ unramifiedLocus R A ↔
    FormallyUnramified.{u_2, u_1} R (Localization.Away f)
have rw : Subsingleton.{u_2 + 1} (LocalizedModule.Away f Ω[A⁄R]) ↔ Subsingleton.{u_2 + 1} Ω[Localization.Away f⁄R]
Tactic: rw [unramifiedLocus_eq_compl_support, Set.subset_compl_comm,
    PrimeSpectrum.basicOpen_eq_zeroLocus_compl, compl_compl,
    ← LocalizedModule.subsingleton_iff_support_subset, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Locus (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
rw : Eq (α := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ Set.univ ↔ FormallyUnramified R A
rw₁ : Eq (α := Set (PrimeSpectrum A)) Set.univᶜ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) Set.univ ↔ FormallyUnramified R A
have rw₂ : Eq (α := Set (PrimeSpectrum A)) ∅ (Module.support A Ω[A⁄R]) ↔ FormallyUnramified R A
Tactic: rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]