awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this : Q'.LiesOver Q
⊢ ¬HPow.hPow (α := P.ResidueField[X]) (β := ℕ)
        (minpoly P.ResidueField (B := Q.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      Polynomial.map (algebraMap R P.ResidueField) p
have this₁ : Q'.LiesOver P
Tactic: have : Q'.LiesOver P := .trans _ Q _
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
⊢ Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
have rw : Eq (α := Subalgebra P.ResidueField (P.ResidueField ⊗[R] S)) P.ResidueField[1 ⊗ₜ[R] x] ⊤
Tactic: rw [← AlgHom.range_eq_top, ← adjoin_singleton_eq_range_aeval]
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
⊢ ¬HPow.hPow (α := P.ResidueField[X]) (β := ℕ)
        (minpoly P.ResidueField (B := Q.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      Polynomial.map (algebraMap R P.ResidueField) p
have this₁ : Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
  (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
Tactic: have : Function.Surjective (aeval (R := P.ResidueField) ((1 : P.ResidueField) ⊗ₜ[R] x)) := by
    rw [← AlgHom.range_eq_top, ← adjoin_singleton_eq_range_aeval]
    simpa using TensorProduct.adjoin_one_tmul_image_eq_top (A := P.ResidueField) _ hp₂
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
⊢ ¬HPow.hPow (α := P.ResidueField[X]) (β := ℕ)
        (minpoly P.ResidueField (B := Q.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
        2 ∣
      Polynomial.map (algebraMap R P.ResidueField) p
have h : Eq.{u_1 + 1} (α := P.ResidueField[X])
  (minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
  (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
    ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
      Q'.ResidueField (R := P.Fiber S)))
Tactic: convert! IsUnramifiedAt.not_minpoly_sq_dvd (A := P.Fiber S) Q' (1 ⊗ₜ x) _ hp₁ this
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
⊢ Eq.{u_1 + 1} (α := P.ResidueField[X])
    (minpoly P.ResidueField (B := Q.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField))
    (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
      ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
        Q'.ResidueField (R := P.Fiber S)))
have h : Eq.{u_1 + 1} (α := P.ResidueField[X])
  (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
    ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField (Q'.ResidueField (R := P.Fiber S)) :
          (a : Q.ResidueField) → Q'.ResidueField)
        ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
      Q'.ResidueField (R := P.Fiber S)))
  (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
    ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
      Q'.ResidueField (R := P.Fiber S)))
Tactic: rw [← minpoly.algHom_eq _
    (IsScalarTower.toAlgHom P.ResidueField Q.ResidueField Q'.ResidueField).injective]
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
⊢ Eq.{u_1 + 1} (α := P.ResidueField[X])
    (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
      ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField (Q'.ResidueField (R := P.Fiber S)) :
            (a : Q.ResidueField) → Q'.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
        Q'.ResidueField (R := P.Fiber S)))
    (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
      ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
        Q'.ResidueField (R := P.Fiber S)))
have h : Eq (α := Algebra P.ResidueField (Q'.ResidueField (R := P.Fiber S))) IsLocalRing.ResidueField.instAlgebra
  (IsLocalRing.ResidueField.algebra (Localization.AtPrime Q'))
Tactic: congr 1
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
h :
  Eq (α := Algebra P.ResidueField (Q'.ResidueField (R := P.Fiber S))) IsLocalRing.ResidueField.instAlgebra
    (IsLocalRing.ResidueField.algebra (Localization.AtPrime Q'))
⊢ Eq.{u_1 + 1} (α := P.ResidueField[X])
    (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
      ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField (Q'.ResidueField (R := P.Fiber S)) :
            (a : Q.ResidueField) → Q'.ResidueField)
          ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
        Q'.ResidueField (R := P.Fiber S)))
    (minpoly P.ResidueField (B := Q'.ResidueField (R := P.Fiber S))
      ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
        Q'.ResidueField (R := P.Fiber S)))
have h₁ : Eq (α := Q'.ResidueField (R := P.Fiber S))
  ((IsScalarTower.toAlgHom P.ResidueField Q.ResidueField (Q'.ResidueField (R := P.Fiber S)) :
        (a : Q.ResidueField) → Q'.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
    Q'.ResidueField (R := P.Fiber S))
  ((algebraMap (P.Fiber S) (Q'.ResidueField (R := P.Fiber S)) : (a : P.Fiber S) → Q'.ResidueField) (1 ⊗ₜ[R] x) :
    Q'.ResidueField (R := P.Fiber S))
Tactic: congr 1
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
⊢ Eq (α := Algebra P.ResidueField (Q'.ResidueField (R := P.Fiber S))) IsLocalRing.ResidueField.instAlgebra
    (IsLocalRing.ResidueField.algebra (Localization.AtPrime Q'))
have h : ∀ (r : IsLocalRing.ResidueField (Localization.AtPrime P)),
  Eq (α := IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q')) :
          (a : IsLocalRing.ResidueField (Localization.AtPrime P)) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        r :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q')) :
          (a : IsLocalRing.ResidueField (Localization.AtPrime P)) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        r :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
Tactic: apply algebra_ext
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
r : IsLocalRing.ResidueField (Localization.AtPrime P)
⊢ Eq (α := IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q')) :
          (a : IsLocalRing.ResidueField (Localization.AtPrime P)) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        r :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
            (IsLocalRing.ResidueField (Localization.AtPrime Q')) :
          (a : IsLocalRing.ResidueField (Localization.AtPrime P)) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        r :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
have h : Eq (α := IsLocalRing.ResidueField (Localization.AtPrime P) →+* IsLocalRing.ResidueField (Localization.AtPrime Q'))
  (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P)) (IsLocalRing.ResidueField (Localization.AtPrime Q')))
  (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P)) (IsLocalRing.ResidueField (Localization.AtPrime Q')))
Tactic: congr 1
-- 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 R
inst_3 : P.IsPrime
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : Q.LiesOver P
inst_6 : IsUnramifiedAt R Q
x : S
p : R[X]
inst_7 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q)
inst_8 : Localization.AtPrime.IsLiesOverAlgebra P Q
hp₁ :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
hp₂ : Eq (α := Subalgebra R S) R[x] ⊤
Q' : Ideal (P.Fiber S) :=
  PrimeSpectrum.asIdeal
    ((PrimeSpectrum.primesOverOrderIsoFiber R S P : (a : (↑(P.primesOver S) : Type u_3)) → PrimeSpectrum (P.Fiber S))
      (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Set (Ideal S)) (P.primesOver S) x) Q ⋯))
this_1 : Q'.LiesOver Q
this_2 : Q'.LiesOver P
this_3 : Algebra (Localization.AtPrime Q) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_4 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q') :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this_5 : IsUnramifiedAt P.ResidueField (A := P.Fiber S) Q'
this :
  Function.Surjective (α := P.ResidueField[X]) (β := P.ResidueField ⊗[R] S)
    (⇑(aeval (1 ⊗ₜ[R] x)) : (a : P.ResidueField[X]) → P.ResidueField ⊗[R] S)
r : IsLocalRing.ResidueField (Localization.AtPrime P)
⊢ Eq (α := IsLocalRing.ResidueField (Localization.AtPrime P) →+* IsLocalRing.ResidueField (Localization.AtPrime Q'))
    (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
      (IsLocalRing.ResidueField (Localization.AtPrime Q')))
    (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
      (IsLocalRing.ResidueField (Localization.AtPrime Q')))
have h : ∀ (x : R),
  Eq (α := IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
              (IsLocalRing.ResidueField (Localization.AtPrime Q')))
            (algebraMap R P.ResidueField) :
          (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        x :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
    ((@RingHom.comp _ P.ResidueField _ _ Semiring.toNonAssocSemiring _
            (algebraMap (IsLocalRing.ResidueField (Localization.AtPrime P))
              (IsLocalRing.ResidueField (Localization.AtPrime Q')))
            (algebraMap R P.ResidueField) :
          (a : R) → IsLocalRing.ResidueField (Localization.AtPrime Q'))
        x :
      IsLocalRing.ResidueField (Localization.AtPrime Q'))
Tactic: ext x
-- 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
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inl : Subsingleton S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: cases subsingleton_or_nontrivial S
-- 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
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
inl : Subsingleton S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr : Nontrivial S → ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: cases subsingleton_or_nontrivial S