[GOAL]
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ⊥ = span R {0}
[PROOFSTEP]
simp
[GOAL]
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionRing K
S : Ideal K
⊢ IsPrincipal S
[PROOFSTEP]
rcases Ideal.eq_bot_or_top S with (rfl | rfl)
[GOAL]
case inl
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionRing K
⊢ IsPrincipal ⊥
case inr
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionRing K
⊢ IsPrincipal ⊤
[PROOFSTEP]
apply bot_isPrincipal
[GOAL]
case inr
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
K : Type u
inst✝ : DivisionRing K
⊢ IsPrincipal ⊤
[PROOFSTEP]
apply top_isPrincipal
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ generator S ∈ S
[PROOFSTEP]
conv_rhs => rw [← span_singleton_generator S]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
| S
[PROOFSTEP]
rw [← span_singleton_generator S]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
| S
[PROOFSTEP]
rw [← span_singleton_generator S]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
| S
[PROOFSTEP]
rw [← span_singleton_generator S]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ generator S ∈ span R {generator S}
[PROOFSTEP]
exact subset_span (mem_singleton _)
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
x : M
⊢ x ∈ S ↔ ∃ s, x = s • generator S
[PROOFSTEP]
simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Ring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : IsPrincipal S
⊢ S = ⊥ ↔ generator S = 0
[PROOFSTEP]
rw [← @span_singleton_eq_bot R M, span_singleton_generator]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
S : Ideal R
inst✝ : IsPrincipal S
x a : R
⊢ x = a • generator S ↔ x = generator S * a
[PROOFSTEP]
simp only [mul_comm, smul_eq_mul]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
S : Ideal R
inst✝ : IsPrincipal S
is_prime : Ideal.IsPrime S
ne_bot : S ≠ ⊥
x✝¹ x✝ : R
⊢ generator S ∣ x✝¹ * x✝ → generator S ∣ x✝¹ ∨ generator S ∣ x✝
[PROOFSTEP]
simpa only [← mem_iff_generator_dvd S] using is_prime.2
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : IsPrincipal (map ϕ N)
x : M
hx : x ∈ N
⊢ generator (map ϕ N) ∣ ↑ϕ x
[PROOFSTEP]
rw [← mem_iff_generator_dvd, Submodule.mem_map]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N : Submodule R M
ϕ : M →ₗ[R] R
inst✝ : IsPrincipal (map ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y, y ∈ N ∧ ↑ϕ y = ↑ϕ x
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
x : M
hx : x ∈ N
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ϕ { val := x, property := (_ : x ∈ O) }
[PROOFSTEP]
rw [← mem_iff_generator_dvd, LinearMap.mem_submoduleImage_of_le hNO]
[GOAL]
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : CommRing R
inst✝¹ : Module R M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
x : M
hx : x ∈ N
⊢ ∃ y yN, ↑ϕ { val := y, property := (_ : y ∈ O) } = ↑ϕ { val := x, property := (_ : x ∈ O) }
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
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
[PROOFSTEP]
intro T x hST hxS hxT
[GOAL]
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
[PROOFSTEP]
cases' (mem_iff_generator_dvd _).1 (hST <| generator_mem S) with z hz
[GOAL]
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
[PROOFSTEP]
cases hpi.mem_or_mem (show generator T * z ∈ S from hz ▸ generator_mem S)
[GOAL]
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
[PROOFSTEP]
case inl h =>
  have hTS : T ≤ S
  rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
  exact (hxS <| hTS hxT).elim
[GOAL]
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
[PROOFSTEP]
case inl h =>
  have hTS : T ≤ S
  rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
  exact (hxS <| hTS hxT).elim
[GOAL]
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
[PROOFSTEP]
have hTS : T ≤ S
[GOAL]
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
[PROOFSTEP]
rwa [← T.span_singleton_generator, Ideal.span_le, singleton_subset_iff]
[GOAL]
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
[PROOFSTEP]
exact (hxS <| hTS hxT).elim
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
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)
[GOAL]
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
[PROOFSTEP]
cases' (mem_iff_generator_dvd _).1 h with y hy
[GOAL]
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
[PROOFSTEP]
have : generator S ≠ 0 := mt (eq_bot_iff_generator_eq_zero _).2 hS
[GOAL]
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
[PROOFSTEP]
rw [← mul_one (generator S), hy, mul_left_comm, mul_right_inj' this] at hz
[GOAL]
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
[PROOFSTEP]
exact hz.symm ▸ T.mul_mem_right _ (generator_mem T)
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
wf : WellFounded EuclideanDomain.r
hmin : WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
⊢ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∣ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h
[PROOFSTEP]
have : x % WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h ∉ {x : R | x ∈ S ∧ x ≠ 0} := fun h₁ =>
  WellFounded.not_lt_min wf _ h h₁ (mod_lt x hmin.2)
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
wf : WellFounded EuclideanDomain.r
hmin : WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : ¬x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ {x | x ∈ S ∧ x ≠ 0}
⊢ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∣ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h
[PROOFSTEP]
have : x % WellFounded.min wf {x : R | x ∈ S ∧ x ≠ 0} h = 0 :=
  by
  simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
  exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
wf : WellFounded EuclideanDomain.r
hmin : WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : ¬x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ {x | x ∈ S ∧ x ≠ 0}
⊢ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h = 0
[PROOFSTEP]
simp only [not_and_or, Set.mem_setOf_eq, not_ne_iff] at this
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
wf : WellFounded EuclideanDomain.r
hmin : WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this : ¬x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∨ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h = 0
⊢ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h = 0
[PROOFSTEP]
exact this.neg_resolve_left <| (mod_mem_iff hmin.1).2 hx
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
wf : WellFounded EuclideanDomain.r
hmin : WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ S ∧ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ≠ 0
x : R
hx : x ∈ S
this✝ : ¬x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∈ {x | x ∈ S ∧ x ≠ 0}
this : x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h = 0
⊢ WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h ∣ x % WellFounded.min wf {x | x ∈ S ∧ x ≠ 0} h
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
a : R
⊢ a ∈ S ↔ a ∈ span R {0}
[PROOFSTEP]
rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
[GOAL]
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬Set.Nonempty {x | x ∈ S ∧ x ≠ 0}
a : R
⊢ a ∈ S ↔ a = 0
[PROOFSTEP]
exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩, fun h₁ => h₁.symm ▸ S.zero_mem⟩
[GOAL]
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsPrincipalIdealRing R
s : Ideal R
⊢ FG s
[PROOFSTEP]
rcases(IsPrincipalIdealRing.principal s).principal with ⟨a, rfl⟩
[GOAL]
case intro
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsPrincipalIdealRing R
a : R
⊢ FG (span R {a})
[PROOFSTEP]
rw [← Finset.coe_singleton]
[GOAL]
case intro
R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : IsPrincipalIdealRing R
a : R
⊢ FG (span R ↑{a})
[PROOFSTEP]
exact ⟨{ a }, SetLike.coe_injective rfl⟩
[GOAL]
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
I : Ideal R
hI : span R {p} < I
⊢ I = ⊤
[PROOFSTEP]
rcases principal I with ⟨a, rfl⟩
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ span R {a} = ⊤
[PROOFSTEP]
erw [Ideal.span_singleton_eq_top]
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : span R {p} < span R {a}
⊢ IsUnit a
[PROOFSTEP]
rcases Ideal.span_singleton_le_span_singleton.1 (le_of_lt hI) with ⟨b, rfl⟩
[GOAL]
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
⊢ IsUnit a
[PROOFSTEP]
refine' (of_irreducible_mul hp).resolve_right (mt (fun hb => _) (not_le_of_lt hI))
[GOAL]
case mk.intro.intro
R : Type u
M : Type v
inst✝¹ : CommRing R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : span R {a * b} < span R {a}
hb : IsUnit b
⊢ span R {a} ≤ span R {a * b}
[PROOFSTEP]
erw [Ideal.span_singleton_le_span_singleton, IsUnit.mul_right_dvd hb]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R), b ∈ factors a → Irreducible b) ∧ Associated (Multiset.prod (factors a)) a
[PROOFSTEP]
unfold factors
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      (b ∈
          if h : a = 0 then ∅
          else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)) →
        Irreducible b) ∧
    Associated
      (Multiset.prod
        (if h : a = 0 then ∅
        else choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a)))
      a
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ (b : R),
      b ∈ choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a) → Irreducible b) ∧
    Associated (Multiset.prod (choose (_ : ∃ f, (∀ (b : R), b ∈ f → Irreducible b) ∧ Associated (Multiset.prod f) a))) a
[PROOFSTEP]
exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)
[GOAL]
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
⊢ a ∈ s
[PROOFSTEP]
rcases(factors_spec a ha).2 with ⟨c, hc⟩
[GOAL]
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ a ∈ s
[PROOFSTEP]
rw [← hc]
[GOAL]
case intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ (b : R), b ∈ factors a → b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : Multiset.prod (factors a) * ↑c = a
⊢ Multiset.prod (factors a) * ↑c ∈ s
[PROOFSTEP]
exact mul_mem (multiset_prod_mem _ hfac) (hunit _)
[GOAL]
R : Type u
M : Type v
S✝ : Type u_1
N : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Ring S✝
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ↑f
S : Submodule R N
hI : IsPrincipal (comap f S)
⊢ S = span R {↑f (generator (comap f S))}
[PROOFSTEP]
rw [← Set.image_singleton, ← Submodule.map_span, IsPrincipal.span_singleton_generator,
  Submodule.map_comap_eq_of_surjective hf]
[GOAL]
R : Type u
M : Type v
S : Type u_1
N : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Ring S
inst✝¹ : Module R M
inst✝ : Module R N
f : R →+* S
hf : Surjective ↑f
I : Ideal S
hI : IsPrincipal (comap f I)
⊢ I = Submodule.span S {↑f (IsPrincipal.generator (comap f I))}
[PROOFSTEP]
rw [Ideal.submodule_span_eq, ← Set.image_singleton, ← Ideal.map_span, Ideal.span_singleton_generator,
  Ideal.map_comap_of_surjective f hf]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
[PROOFSTEP]
obtain ⟨d, hd⟩ := IsPrincipalIdealRing.principal (span ({ x, y } : Set R))
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Submodule.span R {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
[PROOFSTEP]
rw [submodule_span_eq] at hd
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}
[PROOFSTEP]
rw [hd]
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Ideal.span {gcd x y} = Ideal.span {d}
[PROOFSTEP]
suffices Associated d (gcd x y) by
  obtain ⟨D, HD⟩ := this
  rw [← HD]
  exact span_singleton_mul_right_unit D.isUnit _
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
this : Associated d (gcd x y)
⊢ Ideal.span {gcd x y} = Ideal.span {d}
[PROOFSTEP]
obtain ⟨D, HD⟩ := this
[GOAL]
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {gcd x y} = Ideal.span {d}
[PROOFSTEP]
rw [← HD]
[GOAL]
case intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
D : Rˣ
HD : d * ↑D = gcd x y
⊢ Ideal.span {d * ↑D} = Ideal.span {d}
[PROOFSTEP]
exact span_singleton_mul_right_unit D.isUnit _
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ Associated d (gcd x y)
[PROOFSTEP]
apply associated_of_dvd_dvd
[GOAL]
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ gcd x y
[PROOFSTEP]
rw [dvd_gcd_iff]
[GOAL]
case mk.intro.hab
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ x ∧ d ∣ y
[PROOFSTEP]
constructor
[GOAL]
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ x
[PROOFSTEP]
rw [← Ideal.mem_span_singleton, ← hd, Ideal.mem_span_pair]
[GOAL]
case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ d ∣ y
[PROOFSTEP]
rw [← Ideal.mem_span_singleton, ← hd, Ideal.mem_span_pair]
[GOAL]
case mk.intro.hab.left
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = x
[PROOFSTEP]
use 1, 0
[GOAL]
case h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 1 * x + 0 * y = x
[PROOFSTEP]
rw [one_mul, zero_mul, add_zero]
[GOAL]
case mk.intro.hab.right
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ a b, a * x + b * y = y
[PROOFSTEP]
use 0, 1
[GOAL]
case h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ 0 * x + 1 * y = y
[PROOFSTEP]
rw [one_mul, zero_mul, zero_add]
[GOAL]
case mk.intro.hba
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ gcd x y ∣ d
[PROOFSTEP]
obtain ⟨r, s, rfl⟩ : ∃ r s, r * x + s * y = d := by rw [← Ideal.mem_span_pair, hd, Ideal.mem_span_singleton]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y d : R
hd : Ideal.span {x, y} = Ideal.span {d}
⊢ ∃ r s, r * x + s * y = d
[PROOFSTEP]
rw [← Ideal.mem_span_pair, hd, Ideal.mem_span_singleton]
[GOAL]
case mk.intro.hba.intro.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ r * x + s * y
[PROOFSTEP]
apply dvd_add
[GOAL]
case mk.intro.hba.intro.intro.h₁
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ r * x
[PROOFSTEP]
apply dvd_mul_of_dvd_right
[GOAL]
case mk.intro.hba.intro.intro.h₂
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ s * y
[PROOFSTEP]
apply dvd_mul_of_dvd_right
[GOAL]
case mk.intro.hba.intro.intro.h₁.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ x
case mk.intro.hba.intro.intro.h₂.h
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y r s : R
hd : Ideal.span {x, y} = Ideal.span {r * x + s * y}
⊢ gcd x y ∣ y
[PROOFSTEP]
exacts [gcd_dvd_left x y, gcd_dvd_right x y]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
[PROOFSTEP]
simp_rw [mul_comm a, mul_comm b, @eq_comm _ z, ← Ideal.mem_span_pair, ← span_gcd, Ideal.mem_span_singleton]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
a b : R
⊢ ∃ x y, gcd a b = a * x + b * y
[PROOFSTEP]
rw [← gcd_dvd_iff_exists]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ IsCoprime x y
[PROOFSTEP]
rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y
[PROOFSTEP]
rw [← gcd_isUnit_iff]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsUnit (gcd x y)
[PROOFSTEP]
by_contra h
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ False
[PROOFSTEP]
refine' H _ h _ (gcd_dvd_left _ _) (gcd_dvd_right _ _)
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
h : ¬IsUnit (gcd x y)
⊢ gcd x y ≠ 0
[PROOFSTEP]
rwa [Ne, gcd_eq_zero_iff]
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
⊢ x ∣ y ∨ IsCoprime x y
[PROOFSTEP]
refine' or_iff_not_imp_left.2 fun h' => _
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ IsCoprime x y
[PROOFSTEP]
apply isCoprime_of_dvd
[GOAL]
case nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ¬(x = 0 ∧ y = 0)
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
h : Irreducible 0
h' : ¬0 ∣ 0
⊢ False
[PROOFSTEP]
simp at h
[GOAL]
case H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
h : Irreducible x
h' : ¬x ∣ y
⊢ ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
[PROOFSTEP]
rintro z nu - ⟨w, rfl⟩ dy
[GOAL]
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ False
[PROOFSTEP]
refine' h' (dvd_trans _ dy)
[GOAL]
case H.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
y z : R
nu : z ∈ nonunits R
w : R
h : Irreducible (z * w)
h' : ¬z * w ∣ y
dy : z ∣ y
⊢ z * w ∣ z
[PROOFSTEP]
simpa using mul_dvd_mul_left z (isUnit_iff_dvd_one.1 <| (of_irreducible_mul h).resolve_left nu)
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
⊢ IsCoprime x y
[PROOFSTEP]
apply isCoprime_of_dvd x y nonzero
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
⊢ ∀ (z : R), z ∈ nonunits R → z ≠ 0 → z ∣ x → ¬z ∣ y
[PROOFSTEP]
intro z znu znz zx zy
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
⊢ False
[PROOFSTEP]
obtain ⟨i, h1, h2⟩ := WfDvdMonoid.exists_irreducible_factor znu znz
[GOAL]
case intro.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ False
[PROOFSTEP]
apply H i h1
[GOAL]
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ i ∣ x
[PROOFSTEP]
apply dvd_trans h2
[GOAL]
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ z ∣ x
[PROOFSTEP]
assumption
[GOAL]
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ i ∣ y
[PROOFSTEP]
apply dvd_trans h2
[GOAL]
case intro.intro.a
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
x y : R
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y
z : R
znu : z ∈ nonunits R
znz : z ≠ 0
zx : z ∣ x
zy : z ∣ y
i : R
h1 : Irreducible i
h2 : i ∣ z
⊢ z ∣ y
[PROOFSTEP]
assumption
[GOAL]
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ IsCoprime p n → ¬p ∣ n
[PROOFSTEP]
intro co H
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ False
[PROOFSTEP]
apply pp.not_unit
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ IsUnit p
[PROOFSTEP]
rw [isUnit_iff_dvd_one]
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ 1
[PROOFSTEP]
apply IsCoprime.dvd_of_dvd_mul_left co
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n * 1
[PROOFSTEP]
rw [mul_one n]
[GOAL]
case mp
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
co : IsCoprime p n
H : p ∣ n
⊢ p ∣ n
[PROOFSTEP]
exact H
[GOAL]
case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
⊢ ¬p ∣ n → IsCoprime p n
[PROOFSTEP]
intro nd
[GOAL]
case mpr
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ IsCoprime p n
[PROOFSTEP]
apply isCoprime_of_irreducible_dvd
[GOAL]
case mpr.nonzero
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ¬(p = 0 ∧ n = 0)
[PROOFSTEP]
rintro ⟨hp, -⟩
[GOAL]
case mpr.nonzero.intro
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
hp : p = 0
⊢ False
[PROOFSTEP]
exact pp.ne_zero hp
[GOAL]
case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
⊢ ∀ (z : R), Irreducible z → z ∣ p → ¬z ∣ n
[PROOFSTEP]
rintro z zi zp zn
[GOAL]
case mpr.H
R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : GCDMonoid R
p n : R
pp : Irreducible p
nd : ¬p ∣ n
z : R
zi : Irreducible z
zp : z ∣ p
zn : z ∣ n
⊢ False
[PROOFSTEP]
exact nd ((zi.associated_of_dvd pp zp).symm.dvd.trans zn)
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
⊢ nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R
[PROOFSTEP]
simp [Set.eq_empty_iff_forall_not_mem, isPrincipalIdealRing_iff, nonPrincipals_def]
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
⊢ ∃ I, I ∈ nonPrincipals R ∧ ∀ (J : Ideal R), J ∈ c → J ≤ I
[PROOFSTEP]
refine' ⟨sSup c, _, fun J hJ => le_sSup hJ⟩
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
⊢ sSup c ∈ nonPrincipals R
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
⊢ False
[PROOFSTEP]
have hxmem : x ∈ sSup c := hx.symm ▸ Submodule.mem_span_singleton_self x
[GOAL]
case mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
⊢ False
[PROOFSTEP]
obtain ⟨J, hJc, hxJ⟩ := (Submodule.mem_sSup_of_directed ⟨K, hKmem⟩ hchain.directedOn).1 hxmem
[GOAL]
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ False
[PROOFSTEP]
have hsSupJ : sSup c = J := le_antisymm (by simp [hx, Ideal.span_le, hxJ]) (le_sSup hJc)
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
⊢ sSup c ≤ J
[PROOFSTEP]
simp [hx, Ideal.span_le, hxJ]
[GOAL]
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hs : c ⊆ nonPrincipals R
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
⊢ False
[PROOFSTEP]
specialize hs hJc
[GOAL]
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : J ∈ nonPrincipals R
⊢ False
[PROOFSTEP]
rw [← hsSupJ, hx, nonPrincipals_def] at hs
[GOAL]
case mk.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
c : Set (Ideal R)
hchain : IsChain (fun x x_1 => x ≤ x_1) c
K : Ideal R
hKmem : K ∈ c
x : R
hx : sSup c = Submodule.span R {x}
hxmem : x ∈ sSup c
J : Submodule R R
hJc : J ∈ c
hxJ : x ∈ J
hsSupJ : sSup c = J
hs : ¬IsPrincipal (Submodule.span R {x})
⊢ False
[PROOFSTEP]
exact hs ⟨⟨x, rfl⟩⟩
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
⊢ IsPrincipalIdealRing R
[PROOFSTEP]
rw [← nonPrincipals_eq_empty_iff, Set.eq_empty_iff_forall_not_mem]
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
⊢ ∀ (x : Ideal R), ¬x ∈ nonPrincipals R
[PROOFSTEP]
intro J hJ
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
⊢ False
[PROOFSTEP]
obtain ⟨I, Ibad, -, Imax⟩ := zorn_nonempty_partialOrder₀ (nonPrincipals R) nonPrincipals_zorn _ hJ
[GOAL]
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
⊢ False
[PROOFSTEP]
have Imax' : ∀ {J}, I < J → J.IsPrincipal := by
  intro J hJ
  by_contra He
  exact hJ.ne (Imax _ ((nonPrincipals_def R).2 He) hJ.le).symm
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
⊢ ∀ {J : Ideal R}, I < J → IsPrincipal J
[PROOFSTEP]
intro J hJ
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
⊢ IsPrincipal J
[PROOFSTEP]
by_contra He
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J✝ : Ideal R
hJ✝ : J✝ ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
J : Ideal R
hJ : I < J
He : ¬IsPrincipal J
⊢ False
[PROOFSTEP]
exact hJ.ne (Imax _ ((nonPrincipals_def R).2 He) hJ.le).symm
[GOAL]
case intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
⊢ False
[PROOFSTEP]
by_cases hI1 : I = ⊤
[GOAL]
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : I = ⊤
⊢ False
[PROOFSTEP]
subst hI1
[GOAL]
case pos
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
Ibad : ⊤ ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → ⊤ ≤ z → z = ⊤
Imax' : ∀ {J : Ideal R}, ⊤ < J → IsPrincipal J
⊢ False
[PROOFSTEP]
exact Ibad top_isPrincipal
[GOAL]
case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
⊢ False
[PROOFSTEP]
refine' Ibad (H I ⟨hI1, fun {x y} hxy => or_iff_not_imp_right.mpr fun hy => _⟩)
[GOAL]
case neg
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
⊢ x ∈ I
[PROOFSTEP]
obtain ⟨a, ha⟩ : (I ⊔ span { y }).IsPrincipal :=
  Imax'
    (left_lt_sup.mpr (mt I.span_singleton_le_iff_mem.mp hy))
      -- Then `x ∈ I.colon (span {y})`, which is equal to `I` if it's not principal.
[GOAL]
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ x ∈ I
[PROOFSTEP]
suffices He : ¬(I.colon (span { y })).IsPrincipal
[GOAL]
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ I
[PROOFSTEP]
rw [← Imax _ ((nonPrincipals_def R).2 He) fun a ha => Ideal.mem_colon_singleton.2 (mul_mem_right _ _ ha)]
[GOAL]
case neg.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
He : ¬IsPrincipal (colon I (Ideal.span {y}))
⊢ x ∈ colon I (Ideal.span {y})
[PROOFSTEP]
exact Ideal.mem_colon_singleton.2 hxy
[GOAL]
case He
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
⊢ ¬IsPrincipal (colon I (Ideal.span {y}))
[PROOFSTEP]
rintro
  ⟨b, hb⟩
      -- We will show `I` is generated by `a * b`.
[GOAL]
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ False
[PROOFSTEP]
refine (nonPrincipals_def _).1 Ibad ⟨a * b, ?_⟩
[GOAL]
case He.mk.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I = Submodule.span R {a * b}
[PROOFSTEP]
refine' le_antisymm (α := Ideal R) (fun i hi => _) <| (span_singleton_mul_span_singleton a b).ge.trans _
[GOAL]
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
⊢ i ∈ Submodule.span R {a * b}
[PROOFSTEP]
have hisup : i ∈ I ⊔ span { y } := Ideal.mem_sup_left hi
[GOAL]
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
[PROOFSTEP]
have : y ∈ I ⊔ span { y } := Ideal.mem_sup_right (Ideal.mem_span_singleton_self y)
[GOAL]
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : i ∈ I ⊔ Ideal.span {y}
this : y ∈ I ⊔ Ideal.span {y}
⊢ i ∈ Submodule.span R {a * b}
[PROOFSTEP]
erw [ha, mem_span_singleton'] at hisup this
[GOAL]
case He.mk.intro.refine'_1
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
this : ∃ a_1, a_1 * a = y
⊢ i ∈ Submodule.span R {a * b}
[PROOFSTEP]
obtain ⟨v, rfl⟩ := this
[GOAL]
case He.mk.intro.refine'_1.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b i : R
hi : i ∈ I
hisup : ∃ a_1, a_1 * a = i
v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
⊢ i ∈ Submodule.span R {a * b}
[PROOFSTEP]
obtain ⟨u, rfl⟩ := hisup
[GOAL]
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a ∈ Submodule.span R {a * b}
[PROOFSTEP]
have hucolon : u ∈ I.colon (span {v * a}) :=
  by
  rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
  exact mul_mem_right _ _ hi
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u ∈ colon I (Ideal.span {v * a})
[PROOFSTEP]
rw [Ideal.mem_colon_singleton, mul_comm v, ← mul_assoc]
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
⊢ u * a * v ∈ I
[PROOFSTEP]
exact mul_mem_right _ _ hi
[GOAL]
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : u ∈ colon I (Ideal.span {v * a})
⊢ u * a ∈ Submodule.span R {a * b}
[PROOFSTEP]
erw [hb, mem_span_singleton'] at hucolon
[GOAL]
case He.mk.intro.refine'_1.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
u : R
hi : u * a ∈ I
hucolon : ∃ a, a * b = u
⊢ u * a ∈ Submodule.span R {a * b}
[PROOFSTEP]
obtain ⟨z, rfl⟩ := hucolon
[GOAL]
case He.mk.intro.refine'_1.intro.intro.intro
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
z : R
hi : z * b * a ∈ I
⊢ z * b * a ∈ Submodule.span R {a * b}
[PROOFSTEP]
exact mem_span_singleton'.2 ⟨z, by ring⟩
[GOAL]
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x a b v : R
hxy : x * (v * a) ∈ I
hy : ¬v * a ∈ I
ha : I ⊔ Ideal.span {v * a} = Submodule.span R {a}
hb : colon I (Ideal.span {v * a}) = Submodule.span R {b}
z : R
hi : z * b * a ∈ I
⊢ z * (a * b) = z * b * a
[PROOFSTEP]
ring
[GOAL]
case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ Ideal.span {a} * Ideal.span {b} ≤ I
[PROOFSTEP]
rw [← Ideal.submodule_span_eq, ← ha, Ideal.sup_mul, sup_le_iff, span_singleton_mul_span_singleton, mul_comm y,
  Ideal.span_singleton_le_iff_mem]
[GOAL]
case He.mk.intro.refine'_2
R : Type u
M : Type v
inst✝ : CommRing R
H : ∀ (P : Ideal R), IsPrime P → IsPrincipal P
J : Ideal R
hJ : J ∈ nonPrincipals R
I : Ideal R
Ibad : I ∈ nonPrincipals R
Imax : ∀ (z : Ideal R), z ∈ nonPrincipals R → I ≤ z → z = I
Imax' : ∀ {J : Ideal R}, I < J → IsPrincipal J
hI1 : ¬I = ⊤
x y : R
hxy : x * y ∈ I
hy : ¬y ∈ I
a : R
ha : I ⊔ Ideal.span {y} = Submodule.span R {a}
b : R
hb : colon I (Ideal.span {y}) = Submodule.span R {b}
⊢ I * Ideal.span {b} ≤ I ∧ b * y ∈ I
[PROOFSTEP]
exact ⟨mul_le_right, Ideal.mem_colon_singleton.1 <| hb.symm ▸ Ideal.mem_span_singleton_self b⟩


[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y
[PROOFSTEP]
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top
[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
⊢ ⊥ = ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ∀ (y : M), 0 = y
x : M
⊢ x ∈ ⊥ ↔ x ∈ ⊤
[PROOFSTEP]
simp [Submodule.mem_bot, Submodule.mem_top, h x]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsAtom m
[PROOFSTEP]
rw [← Set.isSimpleOrder_Iic_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R { x // x ∈ m } ↔ IsSimpleOrder ↑(Set.Iic m)
[PROOFSTEP]
apply OrderIso.isSimpleOrder_iff
[GOAL]
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R { x // x ∈ m } ≃o ↑(Set.Iic m)
[PROOFSTEP]
exact Submodule.MapSubtype.relIso m
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R (M ⧸ m) ↔ IsCoatom m
[PROOFSTEP]
rw [← Set.isSimpleOrder_Ici_iff_isCoatom]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSimpleModule R (M ⧸ m) ↔ IsSimpleOrder ↑(Set.Ici m)
[PROOFSTEP]
apply OrderIso.isSimpleOrder_iff
[GOAL]
case f
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ Submodule R (M ⧸ m) ≃o ↑(Set.Ici m)
[PROOFSTEP]
exact Submodule.comapMkQRelIso m
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
[PROOFSTEP]
set f : Submodule R B ≃o Set.Iic B := Submodule.MapSubtype.relIso B with hf
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ A ⋖ B ↔ IsSimpleModule R ({ x // x ∈ B } ⧸ Submodule.comap (Submodule.subtype B) A)
[PROOFSTEP]
rw [covby_iff_coatom_Iic hAB, isSimpleModule_iff_isCoatom, ← OrderIso.isCoatom_iff f, hf]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
A B : Submodule R M
hAB : A ≤ B
f : Submodule R { x // x ∈ B } ≃o ↑(Set.Iic B) := Submodule.MapSubtype.relIso B
hf : f = Submodule.MapSubtype.relIso B
⊢ IsCoatom { val := A, property := hAB } ↔
    IsCoatom (↑(Submodule.MapSubtype.relIso B) (Submodule.comap (Submodule.subtype B) A))
[PROOFSTEP]
simp [-OrderIso.isCoatom_iff, Submodule.MapSubtype.relIso, Submodule.map_comap_subtype, inf_eq_right.2 hAB]
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
h : sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
⊢ sSup {a | IsAtom a} = ⊤
[PROOFSTEP]
simp_rw [← h, isSimpleModule_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
simp_rw [isSimpleModule_iff_isAtom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsAtom m} = ⊤
[PROOFSTEP]
exact sSup_atoms_eq_top
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
⊢ IsSemisimpleModule R M → sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
intro
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
a✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R { x // x ∈ m }} = ⊤
[PROOFSTEP]
exact IsSemisimpleModule.sSup_simples_eq_top
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ Function.Injective ↑f ∨ f = 0
[PROOFSTEP]
rw [← ker_eq_bot, ← ker_eq_top]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ ker f = ⊥ ∨ ker f = ⊤
[PROOFSTEP]
apply eq_bot_or_eq_top
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Surjective ↑f ∨ f = 0
[PROOFSTEP]
rw [← range_eq_top, ← range_eq_bot, or_comm]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ range f = ⊥ ∨ range f = ⊤
[PROOFSTEP]
apply eq_bot_or_eq_top
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
by_cases h : f = 0
[GOAL]
case pos
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
right
[GOAL]
case pos.h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : f = 0
⊢ f = 0
[PROOFSTEP]
exact h
[GOAL]
case neg
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsSimpleModule R M
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
h : ¬f = 0
⊢ Function.Bijective ↑f ∨ f = 0
[PROOFSTEP]
exact Or.intro_left _ ⟨injective_of_ne_zero h, surjective_of_ne_zero h⟩
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsCoatom (ker f)
[PROOFSTEP]
rw [← isSimpleModule_iff_isCoatom]
[GOAL]
R : Type u_1
inst✝⁵ : Ring R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R N
f : M →ₗ[R] N
hf : Function.Surjective ↑f
⊢ IsSimpleModule R (M ⧸ ker f)
[PROOFSTEP]
exact IsSimpleModule.congr (f.quotKerEquivOfSurjective hf)
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
⊢ 0 ≠ 1
[PROOFSTEP]
haveI := IsSimpleModule.nontrivial R M
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
⊢ 0 ≠ 1
[PROOFSTEP]
have h := exists_pair_ne M
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : ∃ x y, x ≠ y
⊢ 0 ≠ 1
[PROOFSTEP]
contrapose! h
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : 0 = 1
⊢ ∀ (x y : M), x = y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
h : 0 = 1
x y : M
⊢ x = y
[PROOFSTEP]
simp_rw [ext_iff, one_apply, zero_apply] at h
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
this : Nontrivial M
x y : M
h : ∀ (x : M), 0 = x
⊢ x = y
[PROOFSTEP]
rw [← h x, h y]
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
⊢ ∀ (a : Module.End R M), a ≠ 0 → a * a⁻¹ = 1
[PROOFSTEP]
intro a a0
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
change a * dite _ _ _ = 1
[GOAL]
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
⊢ (a *
      if h : a = 0 then 0
      else
        inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
          (_ :
            Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
          (_ :
            Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)) =
    1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ ↑(a *
          if h : a = 0 then 0
          else
            inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
              (_ :
                Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                  (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
              (_ :
                Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                  (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun))
      x =
    ↑1 x
[PROOFSTEP]
rw [dif_neg a0, mul_eq_comp, one_apply, comp_apply]
[GOAL]
case h
R : Type u_1
inst✝⁶ : Ring R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
m : Submodule R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : DecidableEq (Module.End R M)
inst✝ : IsSimpleModule R M
src✝ : Ring (Module.End R M) := Module.End.ring
a : Module.End R M
a0 : a ≠ 0
x : M
⊢ ↑a
      (↑(inverse a (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
            (_ :
              Function.LeftInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun)
            (_ :
              Function.RightInverse (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).invFun
                (Equiv.ofBijective ↑a (_ : Function.Bijective ↑a)).toFun))
        x) =
    x
[PROOFSTEP]
exact (Equiv.ofBijective _ (bijective_of_ne_zero a0)).right_inv x
[GOAL]
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ Iso (X, X ⊔ Y) (X ⊓ Y, Y)
[PROOFSTEP]
constructor
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, X ⊔ Y).snd } ⧸ Submodule.comap (Submodule.subtype (X, X ⊔ Y).snd) (X, X ⊔ Y).fst) ≃ₗ[R]
    { x // x ∈ (X ⊓ Y, Y).snd } ⧸ Submodule.comap (Submodule.subtype (X ⊓ Y, Y).snd) (X ⊓ Y, Y).fst
[PROOFSTEP]
rw [sup_comm, inf_comm]
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ (X, Y ⊔ X).snd } ⧸ Submodule.comap (Submodule.subtype (X, Y ⊔ X).snd) (X, Y ⊔ X).fst) ≃ₗ[R]
    { x // x ∈ (Y ⊓ X, Y).snd } ⧸ Submodule.comap (Submodule.subtype (Y ⊓ X, Y).snd) (Y ⊓ X, Y).fst
[PROOFSTEP]
dsimp
[GOAL]
case val
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
X Y : Submodule R M
x✝ : X ⋖ X ⊔ Y
⊢ ({ x // x ∈ Y ⊔ X } ⧸ Submodule.comap (Submodule.subtype (Y ⊔ X)) X) ≃ₗ[R]
    { x // x ∈ Y } ⧸ Submodule.comap (Submodule.subtype Y) Y ⊓ Submodule.comap (Submodule.subtype Y) X
[PROOFSTEP]
exact (LinearMap.quotientInfEquivSupQuotient Y X).symm