-- Lean 4 proof step from Mathlib.RingTheory.DiscreteValuationRing.TFAE (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDomain R
inst_3 : IsDedekindDomain R
pos : ∀ (ne_bot : Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
neg neg₁ : ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥), Submodule.IsPrincipal (maximalIdeal R)
neg₂ :
  ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
    (ha₂ : a ≠ 0), Submodule.IsPrincipal (maximalIdeal R)
neg₃ :
  ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
    (ha₂ : a ≠ 0) (hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R)), Submodule.IsPrincipal (maximalIdeal R)
neg₄ :
  ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
    (ha₂ : a ≠ 0) (hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R))
    (this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R)), Submodule.IsPrincipal (maximalIdeal R)
neg₅ :
  ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
    (ha₂ : a ≠ 0) (hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R))
    (this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R))
    (this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}),
    Submodule.IsPrincipal (maximalIdeal R)
neg₆ :
  ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
    (ha₂ : a ≠ 0) (hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R))
    (this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R))
    (this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a})
    (hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = 0),
    Submodule.IsPrincipal (maximalIdeal R)
⊢ Submodule.IsPrincipal (maximalIdeal R)
have neg₇ : ∀ (ne_bot : ¬Eq (α := Ideal R) (maximalIdeal R) ⊥) (a : R) (ha₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) a)
  (ha₂ : a ≠ 0) (hle : LE.le (α := Ideal R) (Ideal.span {a}) (maximalIdeal R))
  (this : Eq (α := Ideal R) (Ideal.radical (Ideal.span {a})) (maximalIdeal R))
  (this : ∃ (n : ℕ), HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) (n : ℕ)
  (hn : Nat.find (p := fun (n : ℕ) ↦ HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ Ideal.span {a}) this = n + 1),
  Submodule.IsPrincipal (maximalIdeal R)
Tactic: classical
  by_cases ne_bot : maximalIdeal R = ⊥
  · rw [ne_bot]; infer_instance
  obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ maximalIdeal R, a ≠ (0 : R) := by
    by_contra! h'; apply ne_bot; rwa [eq_bot_iff]
  have hle : Ideal.span {a} ≤ maximalIdeal R := by rwa [Ideal.span_le, Set.singleton_subset_iff]
  have : (Ideal.span {a}).radical = maximalIdeal R := by
    rw [Ideal.radical_eq_sInf]
    apply le_antisymm
    · exact sInf_le ⟨hle, inferInstance⟩
    · refine
        le_sInf fun I hI =>
          (eq_maximalIdeal <| hI.2.isMaximal (fun e => ha₂ ?_)).ge
      rw [← Ideal.span_singleton_eq_bot, eq_bot_iff, ← e]; exact hI.1
  have : ∃ n, maximalIdeal R ^ n ≤ Ideal.span {a} := by
    rw [← this]; apply Ideal.exists_radical_pow_le_of_fg; exact IsNoetherian.noetherian _
  rcases hn : Nat.find this with - | n
  · have := Nat.find_spec this
    rw [hn, pow_zero, Ideal.one_eq_top] at this
    exact (Ideal.IsMaximal.ne_top inferInstance (eq_top_iff.mpr <| this.trans hle)).elim
  obtain ⟨b, hb₁, hb₂⟩ : ∃ b ∈ maximalIdeal R ^ n, b ∉ Ideal.span {a} := by
    by_contra! h'; rw [Nat.find_eq_iff] at hn; exact hn.2 n n.lt_succ_self fun x hx => h' x hx
  have hb₃ : ∀ m ∈ maximalIdeal R, ∃ k : R, k * a = b * m := by
    intro m hm; rw [← Ideal.mem_span_singleton']; apply Nat.find_spec this
    rw [hn, pow_succ]; exact Ideal.mul_mem_mul hb₁ hm
  have hb₄ : b ≠ 0 := by rintro rfl; apply hb₂; exact zero_mem _
  let K := FractionRing R
  let x : K := algebraMap R K b / algebraMap R K a
  let M := Submodule.map (Algebra.linearMap R K) (maximalIdeal R)
  have ha₃ : algebraMap R K a ≠ 0 := IsFractionRing.to_map_eq_zero_iff.not.mpr ha₂
  by_cases hx : ∀ y ∈ M, x * y ∈ M
  · have := isIntegral_of_smul_mem_submodule M ?_ ?_ x hx
    · obtain ⟨y, e⟩ := IsIntegrallyClosed.algebraMap_eq_of_integral this
      refine (hb₂ (Ideal.mem_span_singleton'.mpr ⟨y, ?_⟩)).elim
      apply IsFractionRing.injective R K
      rw [map_mul, e, div_mul_cancel₀ _ ha₃]
    · rw [Submodule.ne_bot_iff]; refine ⟨_, ⟨a, ha₁, rfl⟩, ?_⟩
      exact (IsFractionRing.to_map_eq_zero_iff (K := K)).not.mpr ha₂
    · apply Submodule.FG.map; exact IsNoetherian.noetherian _
  · have :
        (M.map (DistribSMul.toLinearMap R K x)).comap (Algebra.linearMap R K) = ⊤ := by
      contrapose! hx with h
      rintro m' ⟨m, hm, rfl : algebraMap R K m = m'⟩
      obtain ⟨k, hk⟩ := hb₃ m hm
      have hk' : x * algebraMap R K m = algebraMap R K k := by
        rw [← mul_div_right_comm, ← map_mul, ← hk, map_mul, mul_div_cancel_right₀ _ ha₃]
      exact ⟨k, le_maximalIdeal h ⟨_, ⟨_, hm, rfl⟩, hk'⟩, hk'.symm⟩
    obtain ⟨y, hy₁, hy₂⟩ : ∃ y ∈ maximalIdeal R, b * y = a := by
      rw [Ideal.eq_top_iff_one, Submodule.mem_comap] at this
      obtain ⟨_, ⟨y, hy, rfl⟩, hy' : x * algebraMap R K y = algebraMap R K 1⟩ := this
      rw [map_one, ← mul_div_right_comm, div_eq_one_iff_eq ha₃, ← map_mul] at hy'
      exact ⟨y, hy, IsFractionRing.injective R K hy'⟩
    refine ⟨⟨y, ?_⟩⟩
    apply le_antisymm
    · intro m hm; obtain ⟨k, hk⟩ := hb₃ m hm; rw [← hy₂, mul_comm, mul_assoc] at hk
      rw [← mul_left_cancel₀ hb₄ hk, mul_comm]; exact Ideal.mem_span_singleton'.mpr ⟨_, rfl⟩
    · rwa [Submodule.span_le, Set.singleton_subset_iff]