-- Lean 4 proof step from Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Nonempty.{u_1 + 1} (NormalizedGCDMonoid R)
I : Ideal R
hI :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹ =
    1
a : R
K : Ideal R
ha0 : a ≠ 0
ha0' :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
      (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
        FractionalIdeal (R := R) R⁰ (FractionRing R))
      ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
        FractionalIdeal (R := R) R⁰ (FractionRing R)) =
    1
h :
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑K : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) =
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
        (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
          FractionalIdeal (R := R) R⁰ (FractionRing R))
        ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
      (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹
rwa :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)⁻¹ :
              FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
            (↑K : FractionalIdeal R⁰ (FractionRing R)) =
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
            FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹),
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑K : FractionalIdeal R⁰ (FractionRing R)) =
      spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
rwa₁ :
  ∀
    (h :
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a))⁻¹ :
              FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
            (↑K : FractionalIdeal R⁰ (FractionRing R)) =
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
            FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹),
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑K : FractionalIdeal R⁰ (FractionRing R)) =
      spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
rwa₂ :
  ∀
    (h :
      1 *
          HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
            (↑K : FractionalIdeal R⁰ (FractionRing R)) =
        HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β :=
            FractionalIdeal (R := R) R⁰ (FractionRing R))
            (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
              FractionalIdeal (R := R) R⁰ (FractionRing R))
            ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
          (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹),
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑K : FractionalIdeal R⁰ (FractionRing R)) =
      spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
⊢ HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
have rwa₃ : ∀
  (h :
    HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
        (↑K : FractionalIdeal R⁰ (FractionRing R)) =
      HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (β := FractionalIdeal (R := R) R⁰ (FractionRing R))
          (spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a) :
            FractionalIdeal (R := R) R⁰ (FractionRing R))
          ((↑I : FractionalIdeal (R := R) R⁰ (FractionRing R)) : FractionalIdeal (R := R) R⁰ (FractionRing R)) *
        (↑I : FractionalIdeal R⁰ (FractionRing R))⁻¹),
  HMul.hMul (α := FractionalIdeal (R := R) R⁰ (FractionRing R)) (↑I : FractionalIdeal R⁰ (FractionRing R))
      (↑K : FractionalIdeal R⁰ (FractionRing R)) =
    spanSingleton R⁰ ((algebraMap R (FractionRing R) : (a : R) → FractionRing R) a)
Tactic: rwa [mul_mul_mul_comm, ← spanSingleton_inv, ha0', one_mul, mul_assoc, hI, mul_one] at h
Cleared hypotheses: h