R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : ¬x ∈ S
hxT : x ∈ T
⊢ 1 ∈ T
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
hS : S ≠ ⊥
⊢ ∀ (J : Ideal R) (x : R), S ≤ J → ¬x ∈ S → x ∈ J → 1 ∈ J
intro T x hST hxS hxT
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
hS : S ≠ ⊥
T : Ideal R
x : R
hST : S ≤ T
hxS : ¬x ∈ S
hxT : x ∈ T
⊢ 1 ∈ T
cases' (mem_iff_generator_dvd _).1 (hST <| generator_mem S) with z hz
case intro.inl
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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

case intro.inr
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S)
case intro.inr
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case intro.inl
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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

case intro.inr
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case inl h =>
  have hTS : T ≤ S
  rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
  exact (hxS <| hTS hxT).elim
no goals
case intro.inr
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case inr h =>
  cases' (mem_iff_generator_dvd _).1 h with y hy
  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)
case hTS
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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

R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
have hTS : T ≤ S
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case hTS
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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

R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
no goals
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
exact (hxS <| hTS hxT).elim
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
cases' (mem_iff_generator_dvd _).1 h with y hy
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
no goals
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
S : Ideal R
hpi : IsPrime S
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
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)