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 : 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
⊢ ∑ x ∈ t, (↑(μ x) : R) ∈ I a

Tactic:
sum_mem _ fun x hx => ?_

Premises used: Set.Mem, Ideal.sum_mem
-- 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 : ι) (hx : x ∈ t), (↑(μ x) : R) ∈ I a
⊢ ∑ x ∈ t, (↑(μ x) : R) ∈ I a

Tactic:
refine sum_mem _ fun x hx => ?_

Premises used: Ideal.sum_mem
-- 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
x : ι
hx : x ∈ t
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) (↑(μ x) : R)

Tactic:
have := Submodule.coe_mem (μ x)
-- 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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
x : ι
hx : x ∈ t
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) (↑(μ x) : R)
⊢ ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ x), (↑(μ x) : R) ∈ I i

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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
x : ι
hx : x ∈ t
this : ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ x), (↑(μ x) : R) ∈ I i
refine_1 : a ≠ x
⊢ (↑(μ x) : R) ∈ I a

Tactic:
apply this _ (Finset.mem_cons_self _ _)

Premises used: Finset.mem_cons_self
-- 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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
hx : a ∈ t
this : ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i
⊢ False

Tactic:
hat hx
-- 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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
hx : a ∈ t
this : ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i
⊢ False

Tactic:
exact hat hx
-- 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
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) (↑(μ a) : R)

Tactic:
have := Submodule.coe_mem (μ a)
-- 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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) (↑(μ a) : R)
⊢ ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i

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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
this : ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i
⊢ (↑(μ a) : R) ∈ I b

Tactic:
this _ (Finset.subset_cons _ hb) ab.symm

Premises used: Set.Mem, Finset.subset_cons, Ne.symm
-- 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μ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1
b : ι
hb : b ∈ (↑t : Set ι)
ab : a ≠ b
this : ∀ (i : ι) (i_1 : i ∈ Finset.cons a t hat) (i_2 : i ≠ a), (↑(μ a) : R) ∈ I i
⊢ (↑(μ a) : R) ∈ I b

Tactic:
exact this _ (Finset.subset_cons _ hb) ab.symm

Premises used: Finset.subset_cons, Ne.symm
-- 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
case : 1 ∈ I a ⊔ I b
case₁ case₂ case₃ : ∃ y ∈ I a, ∃ z ∈ I b, y + z = 1
case₄ :
  ∀ (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
refine_1 :
  ∀ (hμ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1) (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b),
    ∑ x ∈ t, (↑(μ x) : R) ∈ I a
refine_2 refine_2₁ :
  ∀ (hμ : ∑ x ∈ t, (↑(μ x) : R) + (↑(μ a) : R) = 1) (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b), (↑(μ a) : R) ∈ I b
⊢ I a ⊔ I b = ⊤

Tactic:
case a4 =>
      rw [eq_top_iff_one, Submodule.mem_sup]
      rw [add_comm] at hμ
      refine ⟨_, ?_, _, ?_, hμ⟩
      · refine sum_mem _ fun x hx => ?_
        have := Submodule.coe_mem (μ x)
        simp only [mem_iInf] at this
        apply this _ (Finset.mem_cons_self _ _)
        rintro rfl
        exact hat hx
      · have := Submodule.coe_mem (μ a)
        simp only [mem_iInf] at this
        exact this _ (Finset.subset_cons _ hb) ab.symm

Premises used: Ideal.sum_mem, add_comm, Ideal.eq_top_iff_one, Ideal.mem_iInf, Submodule.mem_sup, 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
refine_2 :
  ∀ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)) (hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1),
    ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
      Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1
⊢ ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
    Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1

Tactic:
obtain ⟨μ, hμ⟩ := ih.mpr hs

Premises used: Iff.mpr
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
⊢ I a ⊔ ⨅ i ∈ t, I i = ⊤

Tactic:
have := sup_iInf_eq_top fun b hb => Hb b hb (ne_of_mem_of_not_mem hb hat).symm
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
this : I a ⊔ ⨅ i ∈ t, I i = ⊤
⊢ ∃ y ∈ I a, ∃ (z : R), Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) z ∧ y + z = 1

Tactic:
rw [eq_top_iff_one, Submodule.mem_sup] at this

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_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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
this : ∃ y ∈ I a, ∃ (z : R), Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) z ∧ y + z = 1
refine_2 :
  ∀ (u : R) (hu : u ∈ I a) (v : R) (hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v) (huv : u + v = 1),
    ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
      Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1
⊢ ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
    Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := this
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
⊢ ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
    Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1

Tactic:
⟨fun i => if hi : i = a then ⟨v, ?_⟩ else ⟨u * μ i, ?_⟩, ?_⟩

Premises used: HMul.hMul, dite, Subtype.mk, Exists.intro, Subtype.val, Eq
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
refine_2 : ∀ (i : ι) (hi : i = a), Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) v
refine_2₁ :
  ∀ (i : ι) (hi : ¬i = a),
    Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) (u * (↑(μ i) : R))
refine_2₂ :
  Eq.{u_2 + 1} (α := R)
    (∑ i ∈ Finset.cons a t hat,
      (↑((fun (i : ι) ↦
              (if hi : i = a then
                  Subtype.mk (p := fun (x : R) ↦
                    Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) v ⋯
                else
                  Subtype.mk (p := fun (x : R) ↦
                    Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x)
                    (u * (↑(μ i) : R)) ⋯ :
                ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)))
            i) :
        R))
    1
⊢ ∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)),
    Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1

Tactic:
refine ⟨fun i => if hi : i = a then ⟨v, ?_⟩ else ⟨u * μ i, ?_⟩, ?_⟩
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
hi : i = a
refine_2 :
  ∀ (hv : ∀ (i : ι) (i_1 : i ∈ t), v ∈ I i) (i_1 : ι) (i_2 : i_1 ∈ Finset.cons a t hat) (i : i_1 ≠ i), v ∈ I i_1
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) v

Tactic:
simp only [mem_iInf] at hv ⊢

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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι) (i_1 : i ∈ t), v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
⊢ j = i ∨ j ∈ t

Tactic:
rw [Finset.mem_cons, ← hi] at hj

Premises used: Finset.mem_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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι) (i_1 : i ∈ t), v ∈ I i
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
hj₁ : j = i ∨ j ∈ t
⊢ j ≠ i

Tactic:
rw [Finset.mem_cons, ← hi] at hj

Premises used: Finset.mem_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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι) (i_1 : i ∈ t), v ∈ I i
j : ι
hj : j = i ∨ j ∈ t
ij : j ≠ i
⊢ v ∈ I j

Tactic:
hv _ (hj.resolve_left ij)

Premises used: Or.resolve_left
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
huv : u + v = 1
i : ι
hi : i = a
hv : ∀ (i : ι) (i_1 : i ∈ t), v ∈ I i
j : ι
hj : j = i ∨ j ∈ t
ij : j ≠ i
⊢ v ∈ I j

Tactic:
exact hv _ (hj.resolve_left ij)

Premises used: Or.resolve_left
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
hi : ¬i = a
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
hi : ¬i = a
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
refine_2 :
  ∀ (this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1) (i_1 : ι)
    (i_2 : i_1 ∈ Finset.cons a t hat) (i_3 : i_1 ≠ i), u * (↑(μ i) : R) ∈ I i_1
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) (u * (↑(μ 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
hj : j ∈ Finset.cons a t hat
ij : j ≠ i
refine_2 :
  ∀ (hat : j ∉ t) (Hb : ∀ b ∈ (↑t : Set ι), j ≠ b → I j ⊔ I b = ⊤) (hu : u ∈ I j) (hi : ¬i = j)
    (hj : j ∈ Finset.cons j t hat), u * (↑(μ i) : R) ∈ I j
refine_2₁ : ∀ (hj : j ∈ t), u * (↑(μ i) : R) ∈ I j
⊢ u * (↑(μ i) : R) ∈ I j

Tactic:
rcases Finset.mem_cons.mp hj with (rfl | hj)

Premises used: Iff.mp, Finset.mem_cons, rfl
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
ij : j ≠ i
hat : j ∉ t
Hb : ∀ b ∈ (↑t : Set ι), j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
hi : ¬i = j
hj : j ∈ Finset.cons j t hat
⊢ u * (↑(μ i) : R) ∈ I j

Tactic:
mul_mem_right _ _ hu

Premises used: Ideal.mul_mem_right
-- 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 = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
i : ι
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
ij : j ≠ i
hat : j ∉ t
Hb : ∀ b ∈ (↑t : Set ι), j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
hi : ¬i = j
hj : j ∈ Finset.cons j t hat
⊢ u * (↑(μ i) : R) ∈ I j

Tactic:
exact mul_mem_right _ _ hu

Premises used: Ideal.mul_mem_right