-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors (hJ : J ≠ ⊥)
    {L : Ideal R} (hL : L ∈ normalizedFactors I) :
    ↑(idealFactorsEquivOfQuotEquiv f ⟨L, dvd_of_mem_normalizedFactors hL⟩)
      ∈ normalizedFactors J

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
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'

Tactic:
rintro ⟨l, hl⟩ ⟨l', hl'⟩

Result:
case mk.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
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 ⟨l, hl⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l', hl'⟩) ↔
    ↑⟨l, hl⟩ ∣ ↑⟨l', hl'⟩

Proof state:
case mk.mk
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
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 ⟨l, hl⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f).toEquiv ⟨l', hl'⟩) ↔
    ↑⟨l, hl⟩ ∣ ↑⟨l', hl'⟩

Tactic:
apply idealFactorsEquivOfQuotEquiv_is_dvd_iso f

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J

Tactic:
refine mem_normalizedFactors_factor_dvd_iso_of_mem_normalizedFactors hI hJ hL
  (d := (idealFactorsEquivOfQuotEquiv f).toEquiv) ?_

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
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'

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ False

Tactic:
rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ ∅
hI : I = ⊥
⊢ False

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ I ≠ ⊥

Tactic:
intro hI

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I = ⊥
⊢ False

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J

Tactic:
have hI : I ≠ ⊥ := by
  intro hI
  rw [hI, bot_eq_zero, normalizedFactors_zero, ← Multiset.empty_eq_zero] at hL
  exact Finset.not_mem_empty _ hL

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ normalizedFactors I
hI : I ≠ ⊥
⊢ ↑((idealFactorsEquivOfQuotEquiv f) ⟨L, ⋯⟩) ∈ normalizedFactors J

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : IsDedekindDomain A
I : Ideal R
J : Ideal A
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
hJ : J ≠ ⊥
L : Ideal R
hL : L ∈ ∅
hI : I = ⊥
⊢ False

Tactic:
exact Finset.not_mem_empty _ hL

Result:
no goals