-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ_1 : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
hμ :
  Eq.{u_2 + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R) (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R) x : R)
        (↑(μ x) : R))
    1
i : ι
h_1 : i ∈ t
hi : i = Exists.choose (p := Membership.mem t) h
pos :
  (↑(Pi.single (M := fun (i : ι) ↦ ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)) (Exists.choose (p := Membership.mem t) h)
            (Subtype.mk (p := fun (x : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j)
                  x)
                (↑(μ a) : R) ⋯ :
              ↥(⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j))
            (Exists.choose (p := Membership.mem t) h)) :
        R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
            (↑(μ (Exists.choose (p := Membership.mem t) h)) : R) ⋯) :
        R) =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R)
          (Exists.choose (p := Membership.mem t) h) :
        R)
      (↑(μ (Exists.choose (p := Membership.mem t) h)) : R)
pos₁ :
  (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
            (↑(μ a) : R) ⋯) :
        R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
            (↑(μ (Exists.choose (p := Membership.mem t) h)) : R) ⋯) :
        R) =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R)
          (Exists.choose (p := Membership.mem t) h) :
        R)
      (↑(μ (Exists.choose (p := Membership.mem t) h)) : R)
pos₂ :
  (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
            (↑(μ a) : R) ⋯) :
        R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
            (↑(μ (Exists.choose (p := Membership.mem t) h)) : R) ⋯) :
        R) =
    (↑(μ a) : R) + (↑(μ (Exists.choose (p := Membership.mem t) h)) : R)
⊢ (↑(Pi.single (M := fun (i : ι) ↦ ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)) (Exists.choose (p := Membership.mem t) h)
            (Subtype.mk (p := fun (x : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j)
                  x)
                (↑(μ a) : R) ⋯ :
              ↥(⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j))
            i) :
        R) +
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
            (↑(μ i) : R) ⋯) :
        R) =
    HAdd.hAdd (α := R) (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R) i : R)
      (↑(μ i) : R)
have pos₃ : (↑(μ a) : R) +
    (↑(Subtype.mk (p := fun (x : R) ↦
          Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) x)
          (↑(μ (Exists.choose (p := Membership.mem t) h)) : R) sorry) :
      R) =
  (↑(μ a) : R) + (↑(μ (Exists.choose (p := Membership.mem t) h)) : R)
Tactic: rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]