-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.Different (goal)
Goal:
A : Type u_1
B : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsDedekindDomain A
inst_5 : IsDedekindDomain B
inst_6 : IsTorsionFree A B
inst_7 : Module.Finite A B
inst_8 : Algebra.IsSeparable.{u_1, u_3} (FractionRing A) (FractionRing B)
P : Ideal B
inst_9 : P.IsPrime
inl :
  ∀ [inst_10 : Ideal.IsPrime.{u_3} (α := B) ⊥],
    ¬Dvd.dvd (α := Ideal B) ⊥ (differentIdeal A B) ↔ IsUnramifiedAt.{u_1, u_3} A (A := B) ⊥
inr inr₁ : ∀ (hPbot : P ≠ ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
inr₂ : ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
inr₃ :
  ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥)
    (hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥),
    ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
inr₄ inr₅ :
  ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥)
    (hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥)
    (this : P.IsMaximal), ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
inr₆ :
  ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥)
    (hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥)
    (this : P.IsMaximal), ¬P ∣ differentIdeal A B → IsUnramifiedAt A P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
have inr₇ : ∀ (hPbot : P ≠ ⊥) (hp : Ne (α := Ideal A) (Ideal.under A P) ⊥)
  (hp' : ¬Eq.{u_3 + 1} (α := Ideal B) (Ideal.map (F := A →+* B) (algebraMap A B) (Ideal.under A P)) ⊥)
  (this : P.IsMaximal), IsUnramifiedAt A P → ¬P ∣ differentIdeal A B
Tactic: classical
  rcases eq_or_ne P ⊥ with rfl | hPbot
  · simp_rw [← Ideal.zero_eq_bot, zero_dvd_iff]
    simp only [Submodule.zero_eq_bot, differentIdeal_ne_bot, not_false_eq_true, true_iff]
    let K := FractionRing A
    let L := FractionRing B
    have : IsLocalization B⁰ (Localization.AtPrime (⊥ : Ideal B)) := by
      convert!
        (inferInstance :
          IsLocalization (⊥ : Ideal B).primeCompl (Localization.AtPrime (⊥ : Ideal B)))
      ext; simp [Ideal.primeCompl]
    refine (Algebra.FormallyUnramified.iff_of_equiv (A := L)
      ((IsLocalization.algEquiv B⁰ _ _).restrictScalars A)).mp ?_
    have : Algebra.FormallyUnramified K L := by
      rwa [Algebra.FormallyUnramified.iff_isSeparable]
    refine .comp A K L
  have hp : P.under A ≠ ⊥ := mt Ideal.eq_bot_of_comap_eq_bot hPbot
  have hp' := (Ideal.map_eq_bot_iff_of_injective
    (FaithfulSMul.algebraMap_injective A B)).not.mpr hp
  have := Ideal.IsPrime.isMaximal inferInstance hPbot
  let := Localization.AtPrime.algebraOfLiesOver (P.under A) P
  constructor
  · intro H
    · rw [Algebra.isUnramifiedAt_iff_map_eq (p := P.under A)]
      constructor
      · suffices Algebra.IsSeparable (A ⧸ P.under A) (B ⧸ P) by infer_instance
        contrapose H
        exact dvd_differentIdeal_of_not_isSeparable A hp P H
      · rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_one_iff hPbot Ideal.map_comap_le]
        apply Ideal.ramificationIdx_spec
        · simp [Ideal.map_le_iff_le_comap]
        · contrapose H
          rw [← pow_one P, show 1 = 2 - 1 by simp]
          apply pow_sub_one_dvd_differentIdeal _ _ _ hp
          simpa [Ideal.dvd_iff_le] using H
  · intro H
    obtain ⟨Q, h₁, h₂⟩ := Ideal.eq_prime_pow_mul_coprime hp' P
    rw [← Ideal.IsDedekindDomain.ramificationIdx_eq_normalizedFactors_count hp' ‹_› hPbot,
      Ideal.ramificationIdx_eq_one_of_isUnramifiedAt hPbot, pow_one] at h₂
    obtain ⟨h₃, h₄⟩ := (Algebra.isUnramifiedAt_iff_map_eq (p := P.under A) _ _).mp H
    exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable
      A P Q (Ideal.isCoprime_iff_sup_eq.mpr h₁) h₂.symm