awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
refine_1 :
  ∀ (a : ι),
    (∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)),
        Eq.{u_2 + 1} (α := R) (∑ i ∈ {a}, (↑(μ i) : R)) 1) ↔
      (↑{a} : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
⊢ (∃ (μ : (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 = ⊤
have refine_2 : ∀ (a : ι) (s : Finset ι) (h : a ∉ s) (hs : s.Nonempty),
  ((∃ (μ : (i : ι) → ↥(⨅ j ∈ s, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ s, (↑(μ i) : R)) 1) ↔
      (↑s : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) →
    ((∃ (μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a s h, ⨅ (_ : j ≠ i), I j)),
        Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a s h, (↑(μ i) : R)) 1) ↔
      (↑(Finset.cons a s h) : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤)
Tactic: refine h.cons_induction ?_ ?_
-- 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 : ι),
    (∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)),
        Eq.{u_2 + 1} (α := R) (∑ i ∈ {a}, (↑(μ i) : R)) 1) ↔
      (↑{a} : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
have refine_1 : ∀ (a : ι),
  ∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)), (↑(μ a) : R) = 1
Tactic: simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true]
-- 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 : ι),
    ∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)), (↑(μ a) : R) = 1
have refine_1 : ∀ (a i : ι) (h : i = a),
  Membership.mem (γ := Submodule R R) (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j) 1
Tactic: refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩
-- 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 ι
refine_1 :
  ∀ (a i : ι) (h : i = a),
    Membership.mem (γ := Submodule R R) (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j) 1
⊢ ∀ (a : ι),
    ∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)), (↑(μ a) : R) = 1
have refine_1₁ : ∀ (a : ι),
  Eq.{u_2 + 1} (α := R)
    (↑((fun (i : ι) ↦
            (if h : i = a then
                Subtype.mk (p := fun (x : R) ↦
                  Membership.mem (γ := Submodule R R)
                    (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j) x)
                  1 sorry
              else 0 :
              ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)))
          a) :
      R)
    1
Tactic: refine fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩
-- 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)),
      Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1) ↔
    (↑(Finset.cons a t hat) : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
have refine_2 : (∃ (μ : (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) ↔
  ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
Tactic: rw [Finset.coe_cons,
    Set.pairwise_insert_of_symmetric fun i j (h : I i ⊔ I j = ⊤) ↦ (sup_comm _ _).trans h]
-- 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)),
      Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1) ↔
    ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine_2 : (∃ (μ : (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) →
  ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
Tactic: constructor
-- 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 = ⊤
refine_2 :
  (∃ (μ : (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) →
    ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
⊢ (∃ (μ : (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) ↔
    ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine_2₁ : (((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤) →
  ∃ (μ : (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: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
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μ : Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have hμ₁ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
Tactic: rw [Finset.sum_cons] at hμ
Cleared hypotheses: hμ
-- 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine : 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) sorry))
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
              (↑(μ i) : R) sorry)
          i) :
      R))
  1
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
-- 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
refine :
  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
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine₁ : ∀ (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b), I a ⊔ I b = ⊤
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
-- 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
refine :
  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
refine₁ : ∀ (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b), I a ⊔ I b = ⊤
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine₂ : Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) (↑(μ a) : R)
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
-- 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μ : (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1
refine :
  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
refine₁ : ∀ (b : ι) (hb : b ∈ (↑t : Set ι)) (ab : a ≠ b), I a ⊔ I b = ⊤
refine₂ :
  Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) (↑(μ a) : R)
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
have refine₃ : ∀ (i : ι), Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
Tactic: refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
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)
have this₁ : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) (↑(μ a) : R)
Tactic: have := Submodule.coe_mem (μ a)
-- 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_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
this : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) (↑(μ a) : R)
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) (↑(μ a) : R)
have rw : ∀ (this : ∀ (i : ι), Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R))
  (i : ι),
  Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose (p := Membership.mem t) h), I i) (↑(μ a) : R)
Tactic: rw [mem_iInf] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
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
this : ∀ (i : ι), Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R)
i : ι
⊢ Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose (p := Membership.mem t) h), I i) (↑(μ a) : R)
have this₁ : Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R)
Tactic: specialize this i
Cleared hypotheses: this
-- 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_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)
⊢ Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ t), ⨅ (_ : i ≠ Exists.choose (p := Membership.mem t) h), I i) (↑(μ a) : R)
have 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
Tactic: rw [mem_iInf, mem_iInf] at this ⊢
Cleared hypotheses: this
-- 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_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
⊢ (↑(μ a) : R) ∈ I i
have apply : i ≠ a
Tactic: apply this (Finset.subset_cons _ hi)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
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)
have this₁ : Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
Tactic: have := Submodule.coe_mem (μ i)
-- 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_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)
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
have 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
Tactic: simp only [mem_iInf] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
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
have 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
Tactic: rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib]
        at hμ
-- 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
⊢ 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
have 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) sorry))
          (fun (i : ι) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) x)
              (↑(μ i) : R) sorry)
          x) :
      R) =
    HAdd.hAdd (α := R) (Pi.single (M := fun (a : ι) ↦ R) (Exists.choose (p := Membership.mem t) h) (↑(μ a) : R) x : R)
      (↑(μ x) : R)
Tactic: convert! hμ