awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R)
rw :
  ∀ (this : ∀ (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i) (i_1 : i ∈ t)
    (i_2 : i ≠ Exists.choose (p := Membership.mem t) h), (↑(μ a) : R) ∈ I i
⊢ Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose (p := Membership.mem t) h), I i) (↑(μ a) : R)

Tactic:
rw [mem_iInf, mem_iInf] at this ⊢

Premises used: Ideal.mem_iInf
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : ∀ (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i
hi : i ∈ t
_ : i ≠ Exists.choose (p := Membership.mem t) h → (↑(μ a) : R) ∈ I i
⊢ ∀ (i_1 : i ≠ Exists.choose (p := Membership.mem t) h), (↑(μ a) : R) ∈ I i

Tactic:
_
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : ∀ (i_2 : i ∈ Finset.cons a t hat) (i_3 : i ≠ a), (↑(μ a) : R) ∈ I i
hi : i ∈ t
i_1 : i ≠ Exists.choose (p := Membership.mem t) h
apply : i ≠ a
⊢ (↑(μ a) : R) ∈ I i

Tactic:
apply this (Finset.subset_cons _ hi)

Premises used: Finset.subset_cons
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : DecidableEq ι
t : Finset ι
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 : ι
hi : i ∈ t
i_1 : i ≠ Exists.choose (p := Membership.mem t) h
hat : i ∉ t
μ : (i_2 : ι) → ↥(⨅ j ∈ Finset.cons i t hat, ⨅ (_ : j ≠ i_2), I j)
hμ : (↑(μ i) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
this : ∀ (i_2 : i ∈ Finset.cons i t hat) (i_3 : i ≠ i), (↑(μ i) : R) ∈ I i
⊢ False

Tactic:
hat hi
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : DecidableEq ι
t : Finset ι
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 : ι
hi : i ∈ t
i_1 : i ≠ Exists.choose (p := Membership.mem t) h
hat : i ∉ t
μ : (i_2 : ι) → ↥(⨅ j ∈ Finset.cons i t hat, ⨅ (_ : j ≠ i_2), I j)
hμ : (↑(μ i) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
this : ∀ (i_2 : i ∈ Finset.cons i t hat) (i_3 : i ≠ i), (↑(μ i) : R) ∈ I i
⊢ False

Tactic:
exact hat hi
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) (↑(μ a) : R)

Tactic:
case a1 =>
      have := Submodule.coe_mem (μ a)
      rw [mem_iInf] at this ⊢
      --for some reason `simp only [mem_iInf]` times out
      intro i
      specialize this i
      rw [mem_iInf, mem_iInf] at this ⊢
      intro hi _
      apply this (Finset.subset_cons _ hi)
      rintro rfl
      exact hat hi

Premises used: Ideal.mem_iInf, rfl
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)

Tactic:
have := Submodule.coe_mem (μ i)
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
simp :
  ∀ (this : ∀ (i_1 : ι) (i_2 : i_1 ∈ Finset.cons a t hat) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1) (i_1 : ι)
    (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)

Tactic:
simp only [mem_iInf] at this ⊢

Premises used: Ideal.mem_iInf
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ Finset.cons a t hat) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ (↑(μ i) : R) ∈ I j

Tactic:
this _ (Finset.subset_cons _ hj) ij

Premises used: Finset.subset_cons
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ Finset.cons a t hat) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
hj : j ∈ t
ij : j ≠ i
⊢ (↑(μ i) : R) ∈ I j

Tactic:
exact this _ (Finset.subset_cons _ hj) ij

Premises used: Finset.subset_cons
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
i : ι
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)

Tactic:
case a2 =>
      have := Submodule.coe_mem (μ i)
      simp only [mem_iInf] at this ⊢
      intro j hj ij
      exact this _ (Finset.subset_cons _ hj) ij

Premises used: Ideal.mem_iInf
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
⊢ 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

Tactic:
rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib]
        at hμ

Premises used: Exists.choose_spec, Finset.sum_add_distrib, if_pos, Finset.sum_pi_single'
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
⊢ 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

Tactic:
hμ
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
h₁ :
  ∀ x ∈ t,
    (↑(HAdd.hAdd (α := (j : ι) → ↥(⨅ j_1 ∈ t, ⨅ (_ : j_1 ≠ j), I j_1)) (β := (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j))
            (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) ⋯))
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
                (↑(μ i) : R) ⋯)
            x) :
        R) =
      HAdd.hAdd (α := R) (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R) x : R)
        (↑(μ x) : R)
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i ∈ t,
      (↑(HAdd.hAdd (α := (j : ι) → ↥(⨅ j_1 ∈ t, ⨅ (_ : j_1 ≠ j), I j_1)) (β := (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j))
            (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) ⋯))
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
                (↑(μ i) : R) ⋯)
            i) :
        R))
    1

Tactic:
convert! hμ
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
h₁ :
  (↑(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)
⊢ (↑(HAdd.hAdd (α := (j : ι) → ↥(⨅ j_1 ∈ t, ⨅ (_ : j_1 ≠ j), I j_1)) (β := (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j))
          (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) ⋯))
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
              (↑(μ i) : R) ⋯)
          i) :
      R) =
    HAdd.hAdd (α := R) (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R) i : R)
      (↑(μ i) : R)

Tactic:
rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]

Premises used: Submodule.coe_add, Submodule.coe_mk, Pi.add_apply
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
pos :
  ∀ (hi : i = Exists.choose (p := Membership.mem t) h),
    (↑(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)
neg :
  ∀ (hi : ¬i = Exists.choose (p := Membership.mem t) h),
    (↑(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)
⊢ (↑(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)

Tactic:
by_cases hi : i = h.choose

Premises used: Exists.choose
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
neg :
  (↑0 : 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)
neg₁ :
  (↑0 : R) +
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
            (↑(μ i) : R) ⋯) :
        R) =
    0 + (↑(μ i) : R)
neg₂ neg₃ :
  0 +
      (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
            (↑(μ i) : R) ⋯) :
        R) =
    0 + (↑(μ i) : 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)

Tactic:
rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]

Premises used: Pi.single_eq_of_ne, Submodule.coe_zero
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i ∈ t,
      (↑(HAdd.hAdd (α := (j : ι) → ↥(⨅ j_1 ∈ t, ⨅ (_ : j_1 ≠ j), I j_1)) (β := (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j))
            (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) ⋯))
            (fun (i : ι) ↦
              Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
                (↑(μ i) : R) ⋯)
            i) :
        R))
    1

Tactic:
case a3 =>
      rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib]
        at hμ
      convert! hμ
      rename_i i _
      rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
      by_cases hi : i = h.choose
      · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
      · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]

Premises used: Submodule.coe_add, Exists.choose_spec, Finset.sum_add_distrib, Submodule.coe_mk, if_pos, Submodule.coe_zero, Pi.add_apply, Finset.sum_pi_single', Exists.choose, Pi.single_eq_same
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
rw : ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1
⊢ I a ⊔ I b = ⊤

Tactic:
rw [eq_top_iff_one, Submodule.mem_sup]

Premises used: Ideal.eq_top_iff_one, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
rw :
  ∀ (hμ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1) (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b),
    ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1

Tactic:
rw [add_comm] at hμ

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1

Tactic:
⟨_, ?_, _, ?_, hμ⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Coprime.Ideal
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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
refine_1 : ∑ x ∈ t, (↑(μ x) : R) ∈ I a
refine_2 : (↑(μ a) : R) ∈ I b
⊢ ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1

Tactic:
refine ⟨_, ?_, _, ?_, hμ⟩