awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
⊢ Eq (α := Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑t : ↥A) * x) :
      Localization.AtPrime P)
    ((algebraMap (↥A) (Localization.AtPrime P) : (a : ↥A) → Localization.AtPrime P) ((↑s : ↥A) * y) :
      Localization.AtPrime P)
have h : (↑t : ↥A) * x = (↑s : ↥A) * y
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.LocalSubring (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
K : Type u_3
inst_2 : Field K
A : Subring K
P : Ideal ↥A
inst_3 : P.IsPrime
x : ↥A
s : ↥P.primeCompl
y : ↥A
t : ↥P.primeCompl
e :
  Eq (α := K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) x s) :
      K)
    (((IsLocalization.liftAlgHom.{u_3, u_3, u_3, u_3} (A := ↥A) (R := ↥A) (M := P.primeCompl) (S :=
              Localization.AtPrime P) (P := K) (f := Algebra.ofId (↥A) K) ⋯ :
            Localization.AtPrime P →ₐ[↥A] K) :
          (a : Localization.AtPrime P) → K)
        (IsLocalization.mk' (Localization.AtPrime P) y t) :
      K)
H : ∀ (x : ↥P.primeCompl), (↑x : ↥A) ≠ 0
this : (↑x : K) = (↑y : K) * (↑(↑t : ↥A) : K)⁻¹ * (↑(↑s : ↥A) : K)
⊢ (↑t : ↥A) * x = (↑s : ↥A) * y
have h : (↑((↑t : ↥A) * x) : K) = (↑((↑s : ↥A) * y) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ Ideal.IsMaximal (maximalIdeal R)
have rw : 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
Tactic: rw [Ideal.isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
⊢ 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
have left : 1 ∉ maximalIdeal R
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
left : 1 ∉ maximalIdeal R
⊢ 1 ∉ maximalIdeal R ∧ ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
have right : ∀ (J : Ideal R) (x : R), maximalIdeal R ≤ J → x ∉ maximalIdeal R → x ∈ J → 1 ∈ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
h : Membership.mem (γ := Ideal R) (maximalIdeal R) 1
⊢ False
have left : IsUnit.{u_1} (M := R) 1
Tactic: apply h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
h : maximalIdeal R ≤ I
hx : x ∉ maximalIdeal R
H : x ∈ I
⊢ 1 ∈ I
have hx₁ : IsUnit x
Tactic: rw [mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] at hx
Cleared hypotheses: hx, H
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
inst : CommSemiring R
inst_1 : IsLocalRing R
I : Ideal R
x : R
h : maximalIdeal R ≤ I
hx : IsUnit x
H : x ∈ I
⊢ 1 ∈ I
have right : ∀ (u : Rˣ) (H : (↑u : R) ∈ I), 1 ∈ I
Tactic: rcases hx with ⟨u, rfl⟩
Cleared hypotheses: x, hx, H
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsLocalRing R
J : Ideal R
hJ : J ≠ ⊤
⊢ J ≤ maximalIdeal R
have rcases : ∀ (M : Ideal R) (hM1 : M.IsMaximal) (hM2 : J ≤ M), J ≤ maximalIdeal R
Tactic: rcases Ideal.exists_le_maximal J hJ with ⟨M, hM1, hM2⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Square (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R ↔ ¬IsField R
have trans : HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R ↔
  ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R
Tactic: trans ¬ maximalIdeal R ^ 2 = maximalIdeal R
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Square (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
trans :
  HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R ↔
    ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R ↔ ¬IsField R
have trans₁ : ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R ↔ ¬IsField R
Tactic: trans ¬ maximalIdeal R ^ 2 = maximalIdeal R
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Square (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R ↔ ¬IsField R
have rw : ¬HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R ↔ ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
Tactic: rw [IsLocalRing.isField_iff_maximalIdeal_eq, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.MaximalIdeal.Square (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ ¬HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R ↔ ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
have refine : ∀ (h : HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R),
  Eq (α := Ideal R) (maximalIdeal R) ⊥
Tactic: refine Iff.not ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
⊢ ¬IsLocalRing ((i : ι) → R i)
have let : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂), ¬IsLocalRing ((i : ι) → R i)
Tactic: let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (hypothesis)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
⊢ ¬IsLocalRing ((i : ι) → R i)
have ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
Tactic: have ha : ¬IsUnit (fun i ↦ if i = i₁ then 0 else 1 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₁) (by simpa using h.map (Pi.evalRingHom R i₁))
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (hypothesis)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
⊢ ¬IsLocalRing ((i : ι) → R i)
have hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
Tactic: have hb : ¬IsUnit (fun i ↦ if i = i₁ then 1 else 0 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₂) (by simpa [hi.symm] using h.map (Pi.evalRingHom R i₂))
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
⊢ (HAdd.hAdd (α := (i : ι) → R i) (fun (i : ι) ↦ if i = i₁ then 0 else 1) fun (i : ι) ↦ if i = i₁ then 1 else 0) = 1
have h : ∀ (x : ι),
  HAdd.hAdd (α := (i : ι) → R i) (β := (i : ι) → R i) (fun (i : ι) ↦ if i = i₁ then 0 else 1)
      (fun (i : ι) ↦ if i = i₁ then 1 else 0) x =
    1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
x : ι
⊢ HAdd.hAdd (α := (i : ι) → R i) (β := (i : ι) → R i) (fun (i : ι) ↦ if i = i₁ then 0 else 1)
      (fun (i : ι) ↦ if i = i₁ then 1 else 0) x =
    1 x
have h : HAdd.hAdd (α := R x) (if x = i₁ then 0 else 1) (if x = i₁ then 1 else 0) = 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
x : ι
⊢ HAdd.hAdd (α := R x) (if x = i₁ then 0 else 1) (if x = i₁ then 1 else 0) = 1
have h : x = i₁ → HAdd.hAdd (α := R x) 0 1 = 1
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
i₁ i₂ : ι
hi : i₁ ≠ i₂
ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
x : ι
h : x = i₁ → HAdd.hAdd (α := R x) 0 1 = 1
⊢ HAdd.hAdd (α := R x) (if x = i₁ then 0 else 1) (if x = i₁ then 1 else 0) = 1
have h₁ : ¬x = i₁ → HAdd.hAdd (α := R x) 1 0 = 1
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
⊢ ¬IsLocalRing ((i : ι) → R i)
have let : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂), ¬IsLocalRing ((i : ι) → R i)
Tactic: classical
  let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
  have ha : ¬IsUnit (fun i ↦ if i = i₁ then 0 else 1 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₁) (by simpa using h.map (Pi.evalRingHom R i₁))
  have hb : ¬IsUnit (fun i ↦ if i = i₁ then 1 else 0 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₂) (by simpa [hi.symm] using h.map (Pi.evalRingHom R i₂))
  exact not_isLocalRing_def ha hb (by ext; dsimp; split <;> simp)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
let let₁ let₂ : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂), ¬IsLocalRing ((i : ι) → R i)
⊢ ¬IsLocalRing ((i : ι) → R i)
have let₃ : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂) (ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1),
  ¬IsLocalRing ((i : ι) → R i)
Tactic: classical
  let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
  have ha : ¬IsUnit (fun i ↦ if i = i₁ then 0 else 1 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₁) (by simpa using h.map (Pi.evalRingHom R i₁))
  have hb : ¬IsUnit (fun i ↦ if i = i₁ then 1 else 0 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₂) (by simpa [hi.symm] using h.map (Pi.evalRingHom R i₂))
  exact not_isLocalRing_def ha hb (by ext; dsimp; split <;> simp)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
ι : Type u_1
inst : Nontrivial ι
R : ι → Type u_2
inst_1 : (i : ι) → Semiring (R i)
inst_2 : ∀ (i : ι), Nontrivial.{u_2} (R i)
let let₁ let₂ : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂), ¬IsLocalRing ((i : ι) → R i)
let₃ :
  ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂) (ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1),
    ¬IsLocalRing ((i : ι) → R i)
⊢ ¬IsLocalRing ((i : ι) → R i)
have let₄ : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂) (ha : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1)
  (hb : ¬IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0), ¬IsLocalRing ((i : ι) → R i)
Tactic: classical
  let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
  have ha : ¬IsUnit (fun i ↦ if i = i₁ then 0 else 1 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₁) (by simpa using h.map (Pi.evalRingHom R i₁))
  have hb : ¬IsUnit (fun i ↦ if i = i₁ then 1 else 0 : Π i, R i) :=
    fun h ↦ not_isUnit_zero (M₀ := R i₂) (by simpa [hi.symm] using h.map (Pi.evalRingHom R i₂))
  exact not_isLocalRing_def ha hb (by ext; dsimp; split <;> simp)
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ [¬IsLocalRing R, Nontrivial.{u_1} (MaximalSpectrum R),
      ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
have tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
Tactic: tfae_have 1 → 2
  | h => not_subsingleton_iff_nontrivial.mp fun _ ↦ h of_singleton_maximalSpectrum
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
⊢ [¬IsLocalRing R, Nontrivial.{u_1} (MaximalSpectrum R),
      ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
have tfae_2_to_3 : ∀ (a : Nontrivial.{u_1} (MaximalSpectrum R)), ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂
Tactic: tfae_have 2 → 3
  | ⟨⟨m₁, hm₁⟩, ⟨m₂, hm₂⟩, h⟩ => ⟨m₁, m₂, ⟨hm₁, hm₂, fun _ ↦ h (by congr)⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
tfae_2_to_3 :
  ∀ (a : Nontrivial.{u_1} (MaximalSpectrum R)), ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂
⊢ [¬IsLocalRing R, Nontrivial.{u_1} (MaximalSpectrum R),
      ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
have tfae_3_to_1 : ∀ (a : ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂), ¬IsLocalRing R
Tactic: tfae_have 3 → 1
  | ⟨m₁, m₂, ⟨hm₁, hm₂, h⟩⟩ => fun _ ↦ h <| (eq_maximalIdeal hm₁).trans (eq_maximalIdeal hm₂).symm
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
h : ¬IsLocalRing R
⊢ ∃ (K₁ : Type u) (K₂ : Type u) (x : Field K₁) (x_1 : Field K₂) (f : R →+* K₁ × K₂),
    Function.Surjective (α := R) (β := K₁ × K₂) (⇑f : (a : R) → K₁ × K₂)
have obtain : ∀ (m₁ m₂ : Ideal R),
  m₁.IsMaximal →
    m₂.IsMaximal →
      ∀ (hm₁m₂ : m₁ ≠ m₂),
        ∃ (K₁ : Type u) (K₂ : Type u) (x : Field K₁) (x_1 : Field K₂) (f : R →+* K₁ × K₂),
          Function.Surjective (α := R) (β := K₁ × K₂) (⇑f : (a : R) → K₁ × K₂)
Tactic: obtain ⟨m₁, m₂, _, _, hm₁m₂⟩ := (not_isLocalRing_tfae.out 0 2).mp h
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.NonLocalRing (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
h : ¬IsLocalRing R
m₁ m₂ : Ideal R
left : m₁.IsMaximal
left_1 : m₂.IsMaximal
hm₁m₂ : m₁ ≠ m₂
e : R ⧸ m₁ ⊓ m₂ ≃+* (R ⧸ m₁) × R ⧸ m₂ := m₁.quotientInfEquivQuotientProd m₂ ⋯
f : R →+* (R ⧸ m₁) × R ⧸ m₂ := e.toRingHom.comp (Ideal.Quotient.mk (m₁ ⊓ m₂))
⊢ ∃ (K₁ : Type u) (K₂ : Type u) (x : Field K₁) (x_1 : Field K₂) (f : R →+* K₁ × K₂),
    Function.Surjective (α := R) (β := K₁ × K₂) (⇑f : (a : R) → K₁ × K₂)
have h₁ : Function.Surjective (α := R) (β := (R ⧸ m₁) × R ⧸ m₂) (⇑f : (a : R) → (R ⧸ m₁) × R ⧸ m₂)
Tactic: use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (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 R
inst_4 : Module.Finite R S
s : Set S
⊢ Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
have rw : Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
  (span R
    ((⇑(↑(IsScalarTower.toAlgHom R S
                (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
            [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
              [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
        (a : S) → S ⧸ pS) ''
      s))
Tactic: rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (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 R
inst_4 : Module.Finite R S
s : Set S
rw :
  Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (span R
      ((⇑(↑(IsScalarTower.toAlgHom R S
                  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
              [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
                [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
          (a : S) → S ⧸ pS) ''
        s))
⊢ Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
    (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
    (map (σ₁₂ := RingHom.id R)
      (↑(IsScalarTower.toAlgHom R S
            (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
        [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
          [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
      (span R s))
have rw₁ : Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
  (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(↑(IsScalarTower.toAlgHom R S
                  (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
              [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
                [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS) :
          (a : S) → S ⧸ pS) ''
        s)))
Tactic: rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Quotient (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 R
inst_4 : Module.Finite R S
s : Set S
⊢ Eq (α :=
      Submodule.{u_1, u_2} (HasQuotient.Quotient R (B := Ideal R) p)
        (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
      (span (HasQuotient.Quotient R (B := Ideal R) p)
        ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s))
      ⊤ ↔
    Eq (α := Submodule R S) (span R s) ⊤
have H : Eq (α := Submodule R (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p)))
  (Submodule.restrictScalars R (R := HasQuotient.Quotient R (B := Ideal R) p)
    (span (HasQuotient.Quotient R (B := Ideal R) p)
      ((⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) p)) : (a : S) → S ⧸ pS) '' s)))
  (map (σ₁₂ := RingHom.id R)
    (↑(IsScalarTower.toAlgHom R S
          (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) p))) :
      [inst_5 : FunLike (S →ₐ[R] S ⧸ pS) S (S ⧸ pS)] →
        [SemilinearMapClass (S →ₐ[R] S ⧸ pS) (RingHom.id R) S (S ⧸ pS)] → S →ₗ[R] S ⧸ pS)
    (span R s))
Tactic: have H : (span (R ⧸ p) ((Ideal.Quotient.mk (I := pS)) '' s)).restrictScalars R =
      (span R s).map (IsScalarTower.toAlgHom R S (S ⧸ pS) : S →ₗ[R] S ⧸ pS) := by
    rw [map_span, ← restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective,
      LinearMap.coe_coe, IsScalarTower.coe_toAlgHom', Ideal.Quotient.algebraMap_eq]