case pos
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := (_ : L ∣ I) }) ∈ normalizedFactors J

case neg
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := (_ : L ∣ I) }) ∈ normalizedFactors J
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := (_ : L ∣ I) }) ∈ normalizedFactors J
by_cases hI : I = ⊥
case pos.h
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ False
case pos
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := (_ : L ∣ I) }) ∈ normalizedFactors J
exfalso
case pos.h
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ ∅
hI : I = ⊥
⊢ False
case pos.h
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ False
rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
no goals
case pos.h
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ ∅
hI : I = ⊥
⊢ False
exact Finset.not_mem_empty _ hL
case neg
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
case neg
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f) { val := L, property := (_ : L ∣ I) }) ∈ normalizedFactors J
refine mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
  (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_
case neg.mk.mk
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l, property := hl }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l', property := hl' }) ↔
    ↑{ val := l, property := hl } ∣ ↑{ val := l', property := hl' }
case neg
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
⊢ ∀ (l l' : { l // l ∣ I }),
    ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l) ∣ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv l') ↔ ↑l ∣ ↑l'
rintro ⟨l, hl⟩ ⟨l', hl'⟩
case neg.mk.mk
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l, property := hl }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l', property := hl' }) ↔
    ↑{ val := l, property := hl } ∣ ↑{ val := l', property := hl' }
case neg.mk.mk
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l, property := hl }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l', property := hl' }) ↔
    ↑{ val := l, property := hl } ∣ ↑{ val := l', property := hl' }
rw [Subtype.coe_mk, Subtype.coe_mk]
no goals
case neg.mk.mk
R : Type u_2
A : Type u_1
K : Type ?u.1123265
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type ?u.1123802
inst✝⁶ : CommRing B
inst✝⁵ : IsDomain B
inst✝⁴ : IsDedekindDomain B
L✝ : Ideal B
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
inst✝¹ : DecidableEq (Ideal R)
inst✝ : DecidableEq (Ideal A)
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : ¬I = ⊥
l : Ideal R
hl : l ∣ I
l' : Ideal R
hl' : l' ∣ I
⊢ ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l, property := hl }) ∣
      ↑(↑(idealFactorsEquivOfQuotEquiv f).toEquiv { val := l', property := hl' }) ↔
    ↑{ val := l, property := hl } ∣ ↑{ val := l', property := hl' }
apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f