awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
K : Type u_3
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : DivisionRing K
φ : R →+* K
hφ : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := K) (⇑φ : (a : R) → K)
⊢ Eq (α := Ideal R) (RingHom.ker φ) (maximalIdeal R)

Tactic:
IsLocalRing.eq_maximalIdeal <| (RingHom.ker_isMaximal_of_surjective φ) hφ

Premises used: RingHom.ker_isMaximal_of_surjective, IsLocalRing.eq_maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_4
inst : Field R
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
IsLocalRing.isField_iff_maximalIdeal_eq.mp (Field.toIsField R)

Premises used: Field.toIsField, IsLocalRing.isField_iff_maximalIdeal_eq, Iff.mp
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Goal:
R : Type u_1
inst : Ring R
inst_1 : IsLocalRing R
S : Subring R
h_unit : ∀ (x : R) (hx : x ∈ S), IsUnit x → IsUnit (Subtype.mk (p := fun (x : R) ↦ x ∈ S) x hx)
⊢ IsLocalRing.{u_1} ↥S

Tactic:
S.toSubsemiring.isLocalRing_of_unit h_unit

Premises used: Subring.toSubsemiring, Set.Mem, Subsemiring.isLocalRing_of_unit
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
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
trans₁ : ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R ↔ ¬IsField R
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R ↔ ¬IsField R

Tactic:
trans ¬ maximalIdeal R ^ 2 = maximalIdeal R

Premises used: IsLocalRing.maximalIdeal
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
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 ↔
    ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R

Tactic:
simp [lt_iff_le_and_ne, Ideal.pow_le_self]

Premises used: lt_iff_le_and_ne, Ideal.pow_le_self
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
rw :
  ¬HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R ↔ ¬Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ ¬HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 = maximalIdeal R ↔ ¬IsField R

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq, pow_two]

Premises used: pow_two, IsLocalRing.isField_iff_maximalIdeal_eq
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
h : Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
refine :
  ∀ (h : HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R),
    Eq (α := Ideal R) (maximalIdeal R) ⊥
⊢ ¬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]⟩

Premises used: Iff.not, Iff.intro
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
h : HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator (IsNoetherian.noetherian _)
      h.symm (maximalIdeal_le_jacobson _)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, IsNoetherian.noetherian, Eq.symm, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
h : HMul.hMul (α := Ideal R) (maximalIdeal R) (maximalIdeal R) = maximalIdeal R
⊢ Eq (α := Ideal R) (maximalIdeal R) ⊥

Tactic:
exact Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator (IsNoetherian.noetherian _)
      h.symm (maximalIdeal_le_jacobson _)

Premises used: IsLocalRing.maximalIdeal_le_jacobson, IsNoetherian.noetherian, Eq.symm, Submodule.eq_bot_of_eq_ideal_smul_of_le_jacobson_annihilator
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
h : ringKrullDim R ≠ 0
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R

Tactic:
(maximalIdeal_sq_lt_maximalIdeal R).mpr (ringKrullDim_eq_zero_of_isField.mt h)

Premises used: Iff.mpr, Function.mt, IsLocalRing.maximalIdeal_sq_lt_maximalIdeal, ringKrullDim_eq_zero_of_isField
-- Module: Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
h : 0 < ringKrullDim R
⊢ HPow.hPow (α := Ideal R) (β := ℕ) (maximalIdeal R) 2 < maximalIdeal R

Tactic:
IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero h.ne.symm

Premises used: Ne.symm, IsLocalRing.maximalIdeal_sq_lt_of_ringKrullDim_ne_zero, LT.lt.ne
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : Semiring R
a b : R
ha : ¬IsUnit a
hb : ¬IsUnit b
hab : a + b = 1
⊢ ¬IsLocalRing R

Tactic:
fun _ ↦ hb <| (isUnit_or_isUnit_of_add_one hab).resolve_left ha

Premises used: Or.resolve_left, IsLocalRing.isUnit_or_isUnit_of_add_one, Not
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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 : ∀ (i₁ i₂ : ι) (hi : i₁ ≠ i₂), ¬IsLocalRing ((i : ι) → R i)
⊢ ¬IsLocalRing ((i : ι) → R i)

Tactic:
let ⟨i₁, i₂, hi⟩ := exists_pair_ne ι
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
h : IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 0 else 1
⊢ IsUnit.{u_2} (M := R i₁) 0

Tactic:
simpa using h.map (Pi.evalRingHom R i₁)

Premises used: Pi.evalRingHom, IsUnit.map
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
⊢ ¬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₁))
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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
h : IsUnit (M := (i : ι) → R i) fun (i : ι) ↦ if i = i₁ then 1 else 0
⊢ IsUnit.{u_2} (M := R i₂) 0

Tactic:
simpa [hi.symm] using h.map (Pi.evalRingHom R i₂)

Premises used: Ne.symm, Pi.evalRingHom, IsUnit.map
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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
⊢ ¬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₂))
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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
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
⊢ (HAdd.hAdd (α := (i : ι) → R i) (fun (i : ι) ↦ if i = i₁ then 0 else 1) fun (i : ι) ↦ if i = i₁ then 1 else 0) = 1

Tactic:
ext
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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 : HAdd.hAdd (α := R x) (if x = i₁ then 0 else 1) (if x = i₁ then 1 else 0) = 1
⊢ 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:
dsimp
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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
h₁ : ¬x = i₁ → HAdd.hAdd (α := R x) 1 0 = 1
⊢ HAdd.hAdd (α := R x) (if x = i₁ then 0 else 1) (if x = i₁ then 1 else 0) = 1

Tactic:
split
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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) 1 0 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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
⊢ ¬IsLocalRing ((i : ι) → R i)

Tactic:
exact not_isLocalRing_def ha hb (by ext; dsimp; split <;> simp)

Premises used: IsLocalRing.not_isLocalRing_def
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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)
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)
⊢ ¬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)
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Nontrivial R₁
inst_3 : Nontrivial R₂
h : IsUnit (M := R₁ × R₂) (1, 0)
⊢ IsUnit.{u_1} (M := R₁) 0

Tactic:
simpa using h.map (RingHom.snd R₁ R₂)

Premises used: RingHom.snd, IsUnit.map
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Nontrivial R₁
inst_3 : Nontrivial R₂
ha : ¬IsUnit (M := R₁ × R₂) (1, 0)
h : IsUnit (M := R₁ × R₂) (0, 1)
⊢ IsUnit.{u_2} (M := R₂) 0

Tactic:
simpa using h.map (RingHom.fst R₁ R₂)

Premises used: RingHom.fst, IsUnit.map
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Nontrivial R₁
inst_3 : Nontrivial R₂
ha : ¬IsUnit (M := R₁ × R₂) (1, 0)
hb : ¬IsUnit (M := R₁ × R₂) (0, 1)
⊢ HAdd.hAdd (α := R₁ × R₂) (1, 0) (0, 1) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsLocalRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ Nontrivial.{u_1} (MaximalSpectrum R)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)

Tactic:
tfae_have 1 → 2
  | h => not_subsingleton_iff_nontrivial.mp fun _ ↦ h of_singleton_maximalSpectrum
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
⊢ Nontrivial.{u_1} (MaximalSpectrum R)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
⊢ ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
⊢ ∀ (a : Nontrivial.{u_1} (MaximalSpectrum R)), ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
m₁ : Ideal R
hm₁ : m₁.IsMaximal
m₂ : Ideal R
hm₂ : m₂.IsMaximal
h : { asIdeal := m₁, isMaximal := hm₁ : MaximalSpectrum R } ≠ { asIdeal := m₂, isMaximal := hm₂ }
h_1 : m₁ = m₂
⊢ { asIdeal := m₁, isMaximal := hm₁ : MaximalSpectrum R } = { asIdeal := m₂, isMaximal := hm₂ }

Tactic:
congr
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : Nontrivial R
tfae_1_to_2 : ∀ (a : ¬IsLocalRing R), Nontrivial.{u_1} (MaximalSpectrum R)
⊢ ∀ (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)⟩⟩
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
⊢ ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
⊢ ∀ (a : ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂), ¬IsLocalRing R

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
⊢ ∀ (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
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂
tfae_3_to_1 : ∀ (a : ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂), ¬IsLocalRing R
⊢ [¬IsLocalRing R, Nontrivial.{u_1} (MaximalSpectrum R),
      ∃ (m₁ : Ideal R) (m₂ : Ideal R), m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
h : ¬IsLocalRing R
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₂)
⊢ ∃ (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

Premises used: IsLocalRing.not_isLocalRing_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂))
h₁ : Function.Surjective (α := R) (β := (R ⧸ m₁) × R ⧸ m₂) (⇑f : (a : R) → (R ⧸ m₁) × R ⧸ 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:
use R ⧸ m₁, R ⧸ m₂, Ideal.Quotient.field m₁, Ideal.Quotient.field m₂, f

Premises used: Ideal.Quotient.field
-- Module: Mathlib.RingTheory.LocalRing.NonLocalRing
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₂))
⊢ Function.Surjective (α := R) (β := (R ⧸ m₁) × R ⧸ m₂) (⇑f : (a : R) → (R ⧸ m₁) × R ⧸ m₂)

Tactic:
apply Function.Surjective.comp e.surjective Ideal.Quotient.mk_surjective

Premises used: RingEquiv.surjective, Ideal.Quotient.mk_surjective, Function.Surjective.comp
-- 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
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))

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]
-- 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
s : Set S
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))
mp :
  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) ⊤
mpr :
  Eq (α := Submodule R S) (span R 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.{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) ⊤

Tactic:
constructor