awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
a :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Finsupp.linearCombination (HasQuotient.Quotient R (B := Ideal R) p) (⇑(basisQuotient b) : (a : ι) → S ⧸ pS) :
          (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq.{u_2 + 1} (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (⇑((Basis.repr (basisQuotient b) : (a : S ⧸ pS) → ι →₀ R ⧸ p)
                  ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x) :
                Finsupp.{u_4, u_1} ι (HasQuotient.Quotient R (B := Ideal R) p)) :
            (a : ι) → R ⧸ p)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((LinearEquiv.symm (Basis.repr (basisQuotient b)) : (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
simp only [Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply,
    Basis.repr_symm_apply]

Premises used: Finsupp.linearEquivFunOnFinite_symm_coe, LinearEquiv.symm_apply_apply, Module.Basis.repr_symm_apply
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
a :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := HasQuotient.Quotient R (B := Ideal R) p) (β :=
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i)
          ((basisQuotient b : (a : ι) → S ⧸ pS) i :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Finsupp.linearCombination (HasQuotient.Quotient R (B := Ideal R) p) (⇑(basisQuotient b) : (a : ι) → S ⧸ pS) :
          (a : ι →₀ R ⧸ p) → S ⧸ pS)
        ((LinearEquiv.symm
              (Finsupp.linearEquivFunOnFinite (HasQuotient.Quotient R (B := Ideal R) p)
                (HasQuotient.Quotient R (B := Ideal R) p) ι) :
            (a : ι → R ⧸ p) → ι →₀ R ⧸ p)
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R))) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
rw [Finsupp.linearCombination_eq_fintype_linearCombination_apply (R ⧸ p),
    Fintype.linearCombination_apply]

Premises used: Fintype.linearCombination_apply
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
a :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ x_1 : ι,
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ i : ι,
        HSMul.hSMul.{u_1, u_2, u_2} (α := HasQuotient.Quotient R (B := Ideal R) p) (β :=
          HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
          (Function.comp (β := R) (⇑(Ideal.Quotient.mk p) : (a : R) → R ⧸ p)
            (⇑((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i)
          ((basisQuotient b : (a : ι) → S ⧸ pS) i :
            HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
simp only [Function.comp_apply, basisQuotient_apply,
    Ideal.Quotient.mk_smul_mk_quotient_map_quotient, ← Algebra.smul_def]

Premises used: IsLocalRing.basisQuotient_apply, Algebra.smul_def, Function.comp_apply, Ideal.Quotient.mk_smul_mk_quotient_map_quotient
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalRing R
inst_4 : Module.Finite R S
inst_5 : Free R S
ι : Type u_4
inst_6 : Fintype ι
b : Basis ι R S
x : S
i : ι
a :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
        (∑ x_1 : ι,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
a₁ a₂ :
  Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS) x :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))
    (∑ x_1 : ι,
        (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p) : (a : S) → S ⧸ pS)
          (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
            ((((b.repr : (a : S) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) x_1 : R) ((b : (a : ι) → S) x_1 : S)) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))

Tactic:
rw [← map_sum, Basis.sum_repr b x]

Premises used: map_sum, Module.Basis.sum_repr
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
pos : ∀ (hI : I = ⊤), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
neg : ∀ (hI : ¬I = ⊤), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
by_cases hI : I = ⊤
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : I = ⊤
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
simp [hI]
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
have : Nontrivial (R ⧸ I) := Ideal.Quotient.nontrivial_iff.mpr hI
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this : Nontrivial.{u_1} (R ⧸ I)
⊢ IsLocalRing.{u_1} (R ⧸ I)

Tactic:
have := IsLocalRing.of_surjective' (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this : IsLocalRing.{u_1} (R ⧸ I)
⊢ IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)

Tactic:
have := IsLocalHom.of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
neg :
  ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0), ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
obtain ⟨n, hn⟩ := IsArtinianRing.isNilpotent_jacobson_bot (R := R ⧸ I)

Premises used: IsArtinianRing.isNilpotent_jacobson_bot
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
h :
  ∀ (x : R ⧸ I),
    Membership.mem (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) x ↔
      Membership.mem (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I)) x
⊢ Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))

Tactic:
ext x
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
x : R ⧸ I
h :
  ∀ (x : R),
    Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
      Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I))
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)
⊢ Membership.mem (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) x ↔
    Membership.mem (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I)) x

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
x : R
⊢ Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I) ↔
    Membership.mem (α := R ⧸ I) (γ := Ideal (R ⧸ I)) (maximalIdeal (R ⧸ I))
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)

Tactic:
simp [sup_eq_left.mpr (le_maximalIdeal hI)]

Premises used: Iff.mpr, sup_eq_left, IsLocalRing.le_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
⊢ Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))

Tactic:
have : (maximalIdeal R).map (Ideal.Quotient.mk I) = maximalIdeal (R ⧸ I) := by
    ext x
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    simp [sup_eq_left.mpr (le_maximalIdeal hI)]
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this_3 : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
this : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
⊢ HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
rw [jacobson_eq_maximalIdeal _ bot_ne_top, ← this, ← Ideal.map_pow, Ideal.zero_eq_bot,
    Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at hn

Premises used: Ideal.zero_eq_bot, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal, Ideal.mk_ker, Ideal.map_pow, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this_3 : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal (R ⧸ I)) (Ideal.jacobson ⊥) n = 0
this : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
hn₁ : HPow.hPow (α := Ideal R) p n ≤ I
⊢ Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))

Tactic:
rw [jacobson_eq_maximalIdeal _ bot_ne_top, ← this, ← Ideal.map_pow, Ideal.zero_eq_bot,
    Ideal.map_eq_bot_iff_le_ker, Ideal.mk_ker] at hn

Premises used: Ideal.zero_eq_bot, bot_ne_top, IsLocalRing.jacobson_eq_maximalIdeal, Ideal.mk_ker, Ideal.map_pow, Ideal.map_eq_bot_iff_le_ker
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this_3 : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
⟨n, hn⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
I : Ideal R
inst_2 : IsArtinianRing.{u_1} (R ⧸ I)
hI : ¬I = ⊤
this_1 : Nontrivial.{u_1} (R ⧸ I)
this_2 : IsLocalRing.{u_1} (R ⧸ I)
this_3 : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this : Eq (α := Ideal (R ⧸ I)) (Ideal.map (F := R →+* R ⧸ I) (Ideal.Quotient.mk I) p) (maximalIdeal (R ⧸ I))
⊢ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
exact ⟨n, hn⟩
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
⊢ Finite.{u_1 + 1} (R ⧸ I) ↔ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
⟨fun _ ↦ exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I, ?_⟩

Premises used: Iff.intro, IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
refine : (∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I) → Finite.{u_1 + 1} (R ⧸ I)
⊢ Finite.{u_1 + 1} (R ⧸ I) ↔ ∃ (n : ℕ), HPow.hPow (α := Ideal R) p n ≤ I

Tactic:
refine ⟨fun _ ↦ exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I, ?_⟩
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)

Tactic:
have : Finite (R ⧸ maximalIdeal R) := ‹_›
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)
⊢ Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) p n)

Tactic:
have := (Ideal.finite_quotient_pow (IsNoetherian.noetherian (maximalIdeal R)) n)
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)
this : Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) p n)
⊢ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
Finite.of_surjective _ (Ideal.Quotient.factor_surjective hn)

Premises used: Ideal.Quotient.factor_surjective, Finite.of_surjective
-- Module: Mathlib.RingTheory.LocalRing.Quotient
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
inst_3 : Finite.{u_1 + 1} (ResidueField R)
I : Ideal R
n : ℕ
hn : HPow.hPow (α := Ideal R) p n ≤ I
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) p)
this : Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) p n)
⊢ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
exact Finite.of_surjective _ (Ideal.Quotient.factor_surjective hn)

Premises used: Ideal.Quotient.factor_surjective, Finite.of_surjective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : R
⊢ Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) x : ResidueField R)
    ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) x :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Eq (α := Ideal R) (RingHom.ker (F := R →+* ResidueField R) (residue R)) (maximalIdeal R)

Tactic:
Ideal.mk_ker

Premises used: IsLocalRing.residue, IsLocalRing.ResidueField, Ideal.mk_ker
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : R
rw :
  Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* ResidueField R) (residue R)) x ↔
    Membership.mem (γ := Ideal R) (maximalIdeal R) x
rw₁ rw₂ : Membership.mem (γ := Ideal R) (maximalIdeal R) x ↔ Membership.mem (γ := Ideal R) (maximalIdeal R) x
⊢ Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) x : ResidueField R) (0 : ResidueField R) ↔
    Membership.mem (γ := Ideal R) (maximalIdeal R) x

Tactic:
rw [← RingHom.mem_ker, ker_residue]

Premises used: IsLocalRing.ker_residue, RingHom.mem_ker
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
x : R
⊢ Ne (α := ResidueField R) ((residue R : (a : R) → ResidueField R) x : ResidueField R) (0 : ResidueField R) ↔ IsUnit x

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Function.Surjective (α := R) (β := ResidueField R) (⇑(residue R) : (a : R) → ResidueField R)

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
R₁ : Type u_4
R₂ : Type u_5
inst_6 : CommRing R₁
inst_7 : CommRing R₂
inst_8 : Algebra R₁ R₂
inst_9 : Algebra R₁ R
inst_10 : Algebra R₂ R
inst_11 : IsScalarTower R₁ R₂ R
⊢ IsScalarTower.{u_4, u_5, u_1} R₁ R₂ (ResidueField R)

Tactic:
inferInstanceAs <| IsScalarTower R₁ R₂ (_ ⧸ _)

Premises used: _private.0.IsLocalRing.instIsScalarTowerResidueField._proof_1
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
⊢ Eq (α := R →+* ResidueField R) (algebraMap R (ResidueField R)) (residue R)

Tactic:
rfl

Premises used: Ideal.Quotient.mk, Submodule.Quotient.mk, IsLocalRing.residue, rfl
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
⊢ IsLocalHom (R := R) (S := ResidueField R) (F := R →+* ResidueField R) (residue R)

Tactic:
⟨fun _ ha =>
    Classical.not_not.mp (Ideal.Quotient.eq_zero_iff_mem.not.mp (isUnit_iff_ne_zero.mp ha))⟩

Premises used: Classical.not_not, IsLocalHom.mk, Iff.not, isUnit_iff_ne_zero, Ideal.Quotient.eq_zero_iff_mem, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : CommRing S
inst_3 : IsLocalRing S
inst_4 : CommRing T
inst_5 : IsLocalRing T
R₀ : Type u_4
inst_6 : CommRing R₀
inst_7 : Algebra R₀ R
inst_8 : Module.Finite R₀ R
⊢ Module.Finite.{u_4, u_1} R₀ (ResidueField R)

Tactic:
.of_surjective (IsScalarTower.toAlgHom R₀ R _).toLinearMap Ideal.Quotient.mk_surjective

Premises used: AlgHom.toLinearMap, Module.Finite.of_surjective, IsScalarTower.toAlgHom, Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.LocalRing.ResidueField.Basic
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : Field S
f : R →+* S
inst_3 : IsLocalHom (R := R) (S := S) f
⊢ RingHom.comp (β := ResidueField R) (lift f) (residue R) = f

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, rfl