awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)))
    (e.toRingEquiv.toRingHom.comp (algebraMap R (Localization.Away g₀)))

Tactic:
exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm

Premises used: AlgEquiv.toAlgHom, AlgHom.comp_algebraMap_of_tower, Eq.symm
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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))

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
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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_4 : 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₀)))
this : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))
e' : AlgEquiv.{u_1, u_3, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀) (Localization.Away (f * g)) :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ 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:
⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩

Premises used: HMul.hMul, Ideal.IsPrime.mul_notMem, Algebra.IsStandardEtale.of_equiv, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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_4 : 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₀)))
this : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))
e' : AlgEquiv.{u_1, u_3, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀) (Localization.Away (f * g)) :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ ∃ 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:
exact ⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩
-- Module: Mathlib.RingTheory.Unramified.Locus
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
⊢ FormallyUnramified.{u_3, u_2} (Localization.AtPrime p) (Localization.AtPrime P)

Tactic:
have : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P) :=
    .of_restrictScalars A _ _
-- Module: Mathlib.RingTheory.Unramified.Locus
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_1 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : FormallyUnramified.{u_3, u_2} (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsUnramifiedAt R P

Tactic:
FormallyUnramified.comp R (Localization.AtPrime p) _

Premises used: Localization.AtPrime, Algebra.FormallyUnramified.comp
-- Module: Mathlib.RingTheory.Unramified.Locus
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_1 : Algebra.{u_2, u_3} (Localization.AtPrime p) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver p P
this : FormallyUnramified.{u_3, u_2} (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsUnramifiedAt R P

Tactic:
exact FormallyUnramified.comp R (Localization.AtPrime p) _

Premises used: Localization.AtPrime, Algebra.FormallyUnramified.comp
-- Module: Mathlib.RingTheory.Unramified.Locus
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 B
inst_7 : P.IsPrime
inst_8 : IsUnramifiedAt R P
⊢ IsUnramifiedAt A P

Tactic:
FormallyUnramified.of_restrictScalars R _ _

Premises used: Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.RingTheory.Unramified.Locus
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 R
inst_7 : p.IsPrime
q : Ideal A
inst_8 : q.IsPrime
inst_9 : q.LiesOver p
inst_10 : IsUnramifiedAt R q
inst_11 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q)
inst_12 : Localization.AtPrime.IsLiesOverAlgebra p q
⊢ FormallyUnramified.{u_2, u_1} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
.of_restrictScalars R _ _

Premises used: Algebra.FormallyUnramified.of_restrictScalars
-- Module: Mathlib.RingTheory.Unramified.Locus
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'
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 ⋯;
    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')
⊢ Function.Surjective (α := Localization.AtPrime Q) (β := Localization.AtPrime (R := P.Fiber A) Q')
    (⇑f₀ : (a : Localization.AtPrime Q) → Localization.AtPrime Q')

Tactic:
subst hQ'
-- Module: Mathlib.RingTheory.Unramified.Locus
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 (P.Fiber A)
inst_4 : Q'.IsPrime
inst_5 : Ideal.IsPrime (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')
inst_6 :
  Ideal.LiesOver (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q') P
inst_7 :
  IsUnramifiedAt R (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')
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 ⋯
⊢ 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:
P.surjectiveOnStalks_residueField.baseChange' _ _

Premises used: Set.Mem, setOf, Ideal.surjectiveOnStalks_residueField, RingHom.SurjectiveOnStalks.baseChange'
-- Module: Mathlib.RingTheory.Unramified.Locus
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 (P.Fiber A)
inst_4 : Q'.IsPrime
inst_5 : Ideal.IsPrime (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')
inst_6 :
  Ideal.LiesOver (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q') P
inst_7 :
  IsUnramifiedAt R (Ideal.comap (F := A →+* P.ResidueField ⊗[R] A) (AlgHom.toRingHom TensorProduct.includeRight) Q')
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 ⋯
⊢ 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:
exact P.surjectiveOnStalks_residueField.baseChange' _ _

Premises used: Ideal.surjectiveOnStalks_residueField, RingHom.SurjectiveOnStalks.baseChange'
-- Module: Mathlib.RingTheory.Unramified.Locus
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')

Tactic:
have hf₀ : Function.Surjective f₀ := by
    subst hQ'; exact P.surjectiveOnStalks_residueField.baseChange' _ _
-- Module: Mathlib.RingTheory.Unramified.Locus
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₀ ⋯
x : Localization.AtPrime Q
⊢ Eq (α := Localization.AtPrime (R := P.Fiber A) Q')
    ((f : (a : P.Fiber (Localization.AtPrime Q)) → Localization.AtPrime Q') (1 ⊗ₜ[R] x) :
      Localization.AtPrime (R := P.Fiber A) Q')
    ((f₀ : (a : Localization.AtPrime Q) → Localization.AtPrime Q') x : Localization.AtPrime (R := P.Fiber A) Q')

Tactic:
simp [f]
-- Module: Mathlib.RingTheory.Unramified.Locus
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₀ ⋯
⊢ 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]⟩
-- Module: Mathlib.RingTheory.Unramified.Locus
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₀ ⋯
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')
⊢ IsUnramifiedAt P.ResidueField (A := P.Fiber A) Q'

Tactic:
.of_surjective _ hf

Premises used: Algebra.FormallyUnramified.of_surjective
-- Module: Mathlib.RingTheory.Unramified.Locus
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₀ ⋯
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')
⊢ IsUnramifiedAt P.ResidueField (A := P.Fiber A) Q'

Tactic:
exact .of_surjective _ hf
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
h :
  ∀ (p : PrimeSpectrum A),
    Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
      Membership.mem (γ := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ p
⊢ Eq (α := Set (PrimeSpectrum A)) (unramifiedLocus R A) (Module.support A Ω[A⁄R])ᶜ

Tactic:
ext p
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
h :
  Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Subsingleton.{u_2 + 1} (LocalizedModule p.asIdeal.primeCompl Ω[A⁄R])
⊢ Membership.mem (γ := Set (PrimeSpectrum A)) (unramifiedLocus R A) p ↔
    Membership.mem (γ := Set (PrimeSpectrum A)) (Module.support A Ω[A⁄R])ᶜ p

Tactic:
simp only [Set.mem_compl_iff, Module.notMem_support_iff]

Premises used: Module.notMem_support_iff, Set.mem_compl_iff
-- Module: Mathlib.RingTheory.Unramified.Locus
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
p : PrimeSpectrum A
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])
⊢ 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))