awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
x : ResidueField S
⊢ ∃ (a : (ResidueField R)[X]),
    ((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        a =
      x
have mpr : ∀ (s : S),
  ∃ (a : (ResidueField R)[X]),
    Eq.{u_2 + 1} (α := ResidueField S)
      (((aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
            (a : (ResidueField R)[X]) → ResidueField S)
          a :
        ResidueField S)
      ((residue S : (a : S) → ResidueField S) s : ResidueField S)
Tactic: obtain ⟨s, rfl⟩ := residue_surjective (R := S) x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
s : S
⊢ ∃ (a : (ResidueField R)[X]),
    Eq.{u_2 + 1} (α := ResidueField S)
      (((aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
            (a : (ResidueField R)[X]) → ResidueField S)
          a :
        ResidueField S)
      ((residue S : (a : S) → ResidueField S) s : ResidueField S)
have mpr : ∀ (p : R[X]),
  ∃ (a : (ResidueField R)[X]),
    Eq.{u_2 + 1} (α := ResidueField S)
      (((aeval ((residue S : (a : S) → ResidueField S) β) :
              AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
            (a : (ResidueField R)[X]) → ResidueField S)
          a :
        ResidueField S)
      ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
Tactic: obtain ⟨p, rfl⟩ := hβ_gen s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β : S
hβ_gen : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R[X]) (β := S) (⇑(aeval β) : (a : R[X]) → S)
p : R[X]
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) p) :
      ResidueField S)
    ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
have rw : Eq (α := ResidueField S) ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
  ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) p) : ResidueField S)
Tactic: rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl p β]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
have obtain : ∀ (β₀ : ResidueField S)
  (hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤),
  ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
Tactic: obtain ⟨β₀, hβ₀⟩ := Field.exists_primitive_element (ResidueField R) (ResidueField S)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
have obtain : ∀ (β : S) (hβ : (residue S : (a : S) → ResidueField S) β = β₀), ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
Tactic: obtain ⟨β, hβ⟩ := residue_surjective (R := S) β₀
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
⊢ ∃ (β : S), Eq (α := Subalgebra R S) R[β] ⊤
have refine : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
  (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
Tactic: refine ⟨β, adjoin_residue_eq_top_iff_adjoin_eq_top β |>.mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
have rw : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)[β₀] ⊤
Tactic: rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
rw : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)[β₀] ⊤
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
have rw₁ : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (IntermediateField.toSubalgebra (ResidueField R)⟮β₀⟯)
  ⊤
Tactic: rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
rw : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)[β₀] ⊤
rw₁ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (IntermediateField.toSubalgebra (ResidueField R)⟮β₀⟯) ⊤
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
have rw₂ : Eq.{u_2 + 1} (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (IntermediateField.toSubalgebra ⊤) ⊤
Tactic: rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : FormallyUnramified R S
β₀ : ResidueField S
hβ₀ : Eq (α := IntermediateField.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)⟮β₀⟯ ⊤
β : S
hβ : (residue S : (a : S) → ResidueField S) β = β₀
rw : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (ResidueField R)[β₀] ⊤
rw₁ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (IntermediateField.toSubalgebra (ResidueField R)⟮β₀⟯) ⊤
rw₂ : Eq.{u_2 + 1} (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) (IntermediateField.toSubalgebra ⊤) ⊤
⊢ Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
have rw₃ : Eq.{u_2 + 1} (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S)) ⊤ ⊤
Tactic: rw [hβ,
    ← IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.of_finite _ _),
    hβ₀, IntermediateField.top_toSubalgebra]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
have this : Module.Free R S
Tactic: have : Module.Free R S := Module.free_of_flat_of_isLocalRing
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
have refine_2 : ∀
  (e :
    HasQuotient.Quotient S (B := Ideal S)
        (Ideal.map (F := R →+* S) (algebraMap R S)
          (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)),
  Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
Tactic: have e := AddEquiv.toLinearEquiv (R := R ⧸ maximalIdeal R) (Ideal.quotEquivOfEq <|
      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv
    ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
refine_2 :
  ∀
    (e :
      HasQuotient.Quotient S (B := Ideal S)
          (Ideal.map (F := R →+* S) (algebraMap R S)
            (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)),
    Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
have refine_1 : ∀ (c : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
  (x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))),
  ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (c • x) =
    HSMul.hSMul (β := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) c
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          x :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
Tactic: have e := AddEquiv.toLinearEquiv (R := R ⧸ maximalIdeal R) (Ideal.quotEquivOfEq <|
      Algebra.FormallyUnramified.map_maximalIdeal (R := R) (S := S)).toAddEquiv
    ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
e :
  HasQuotient.Quotient S (B := Ideal S)
      (Ideal.map (F := R →+* S) (algebraMap R S)
        (maximalIdeal R)) ≃ₗ[HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)]
    HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)
⊢ Module.finrank R S = Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
have refine_2 : Module.finrank.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
    (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))) =
  Module.finrank.{u_1, u_2} (ResidueField R) (ResidueField S)
Tactic: rw [← finrank_quotient_map (R := R) (S := S)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
this : Module.Free R S
r : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)
x : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R))
⊢ ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (r • x) =
    HSMul.hSMul (β := HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) r
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq ⋯) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          x :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
have refine_1 : ∀ (r : R),
  ((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
            HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
        (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
      (HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
        ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
          HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
        x) =
    HSMul.hSMul (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R)) (β :=
      HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) r :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (((RingEquiv.toAddEquiv (Ideal.quotEquivOfEq sorry) :
              HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (maximalIdeal R)) ≃+
                HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S)) :
            (a : S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R)) → S ⧸ maximalIdeal S)
          x :
        HasQuotient.Quotient S (B := Ideal S) (maximalIdeal S : Ideal S))
Tactic: obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
⊢ Eq (α := (ResidueField R)[X]) (map (residue R) (minpoly R β))
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have h : Monic (minpoly R β)
Tactic: have h := minpoly.monic <| Algebra.IsIntegral.isIntegral (R:=R) β
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
⊢ Eq (α := (ResidueField R)[X]) (map (residue R) (minpoly R β))
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_1 : Eq.{u_2 + 1} (α := ResidueField S)
  (((aeval ((residue S : (a : S) → ResidueField S) β) :
          AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
        (a : (ResidueField R)[X]) → ResidueField S)
      (map (residue R) (minpoly R β)) :
    ResidueField S)
  (0 : ResidueField S)
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
refine_1 :
  Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) (minpoly R β)) :
      ResidueField S)
    (0 : ResidueField S)
⊢ Eq (α := (ResidueField R)[X]) (map (residue R) (minpoly R β))
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_2 : natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
  natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
Tactic: refine eq_of_monic_of_dvd_of_natDegree_le
    (minpoly.monic <| Algebra.IsIntegral.isIntegral <| residue S β)
    (h.map _) (minpoly.dvd (ResidueField R) (residue S β) ?_) ?_
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
⊢ Eq.{u_2 + 1} (α := ResidueField S)
    (((aeval ((residue S : (a : S) → ResidueField S) β) :
            AlgHom.{u_1, u_1, u_2} (ResidueField R) (ResidueField R)[X] (ResidueField S)) :
          (a : (ResidueField R)[X]) → ResidueField S)
        (map (residue R) (minpoly R β)) :
      ResidueField S)
    (0 : ResidueField S)
have refine_1 : Eq (α := ResidueField S)
  ((residue S : (a : S) → ResidueField S) ((aeval β : (a : R[X]) → S) (minpoly R β)) : ResidueField S)
  (0 : ResidueField S)
Tactic: rw [← map_aeval_eq_aeval_map (ψ := residue S) (φ := residue R) rfl]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have this : Module.Free R S
Tactic: have : Module.Free R S := Module.free_of_flat_of_isLocalRing
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
this : Module.Free R S
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have hβ₀ : Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
  (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
Tactic: have hβ₀ := (adjoin_residue_eq_top_iff_adjoin_eq_top β).mpr hadj
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Etale (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing S
inst_4 : IsLocalRing R
inst_5 : Module.Finite R S
inst_6 : FaithfulSMul R S
inst_7 : Etale R S
β : S
hadj : Eq (α := Subalgebra R S) R[β] ⊤
h : Monic (minpoly R β)
this : Module.Free R S
hβ₀ :
  Eq (α := Subalgebra.{u_1, u_2} (ResidueField R) (ResidueField S))
    (ResidueField R)[((residue S : (a : S) → ResidueField S) β : ResidueField S)] ⊤
⊢ natDegree (R := ResidueField R) (map (residue R) (minpoly R β)) ≤
    natDegree.{u_1} (R := ResidueField R)
      (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
have refine_2 : natDegree (minpoly R β) ≤
  natDegree.{u_1} (R := ResidueField R)
    (minpoly (ResidueField R) (B := ResidueField S) ((residue S : (a : S) → ResidueField S) β : ResidueField S))
Tactic: rw [h.natDegree_map _,
      ← (IsAdjoinRootMonic.mkOfAdjoinEqTop' hadj).finrank,
      finrank_eq_finrank_residueField,
      (IsAdjoinRootMonic.mkOfAdjoinEqTop' hβ₀).finrank]