-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem to_maximal_ideal [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Ideal R}
    [hpi : IsPrime S] (hS : S ≠ ⊥) : IsMaximal S :=
  isMaximal_iff.2
    ⟨(ne_top_iff_one S).1 hpi.1, by
      intro T x hST hxS hxT
      obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)
      cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
      | inl h =>
        have hTS : T ≤ S

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ T ≤ S

Tactic:
rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
⊢ 1 ∈ T

Tactic:
obtain ⟨z, hz⟩ := (mem_iff_generator_dvd _).1 (hST <| generator_mem S)

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
⊢ 1 ∈ T

Proof state:
case intro.inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
⊢ 1 ∈ T

Tactic:
have hTS : T ≤ S := by
  rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]

Result:
case intro.inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
hTS : T ≤ S
⊢ 1 ∈ T

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
⊢ 1 ∈ T

Tactic:
cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S) with
| inl h =>
  have hTS : T ≤ S := by
    rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
  exact (hxS <| hTS hxT).elim
| inr h =>
  obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h
  have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
  rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
  exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)

Result:
no goals

Proof state:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ 1 ∈ T

Tactic:
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS

Result:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
⊢ ∀ (J : Ideal R) (x : R), S ≤ J → x ∉ S → x ∈ J → 1 ∈ J

Tactic:
intro T x hST hxS hxT

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
⊢ 1 ∈ T

Proof state:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz

Result:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : 1 = generator T * y
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Proof state:
case intro.inr
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
⊢ 1 ∈ T

Tactic:
obtain ⟨y, hy⟩ := (mem_iff_generator_dvd _).1 h

Result:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : z ∈ S
y : R
hy : z = generator S * y
⊢ 1 ∈ T

Proof state:
case intro.inl
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
hz : generator S = generator T * z
h : generator T ∈ S
hTS : T ≤ S
⊢ 1 ∈ T

Tactic:
exact (hxS <| hTS hxT).elim

Result:
no goals

Proof state:
case intro.inr.intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : S.IsPrime
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : x ∉ S
hxT : x ∈ T
z : R
h : z ∈ S
y : R
hz : 1 = generator T * y
hy : z = generator S * y
this : generator S ≠ 0
⊢ 1 ∈ T

Tactic:
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)

Result:
no goals