awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (x + z * y) y

Tactic:
mul_comm z y ▸ h.add_mul_left_left z

Premises used: IsRelPrime.add_mul_left_left, Eq.rec, mul_comm, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime x (y + x * z)

Tactic:
(h.symm.add_mul_left_left z).symm

Premises used: IsRelPrime.add_mul_left_left, IsRelPrime.symm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime x (y + z * x)

Tactic:
(h.symm.add_mul_right_left z).symm

Premises used: IsRelPrime.symm, IsRelPrime.add_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (y * z + x) y

Tactic:
add_comm x _ ▸ h.add_mul_left_left z

Premises used: IsRelPrime.add_mul_left_left, Eq.rec, add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime (z * y + x) y

Tactic:
add_comm x _ ▸ h.add_mul_right_left z

Premises used: Eq.rec, add_comm, IsRelPrime.add_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime x (x * z + y)

Tactic:
add_comm y _ ▸ h.add_mul_left_right z

Premises used: IsRelPrime.add_mul_left_right, Eq.rec, add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
z : R
⊢ IsRelPrime x (z * x + y)

Tactic:
add_comm y _ ▸ h.add_mul_right_right z

Premises used: Eq.rec, IsRelPrime.add_mul_right_right, add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (x + y * z) y ↔ IsRelPrime x y

Tactic:
⟨of_add_mul_left_left, fun h ↦ h.add_mul_left_left z⟩

Premises used: IsRelPrime.add_mul_left_left, IsRelPrime.of_add_mul_left_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (x + z * y) y ↔ IsRelPrime x y

Tactic:
⟨of_add_mul_right_left, fun h ↦ h.add_mul_right_left z⟩

Premises used: IsRelPrime.of_add_mul_right_left, Iff.intro, IsRelPrime.add_mul_right_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (y + x * z) ↔ IsRelPrime x y

Tactic:
⟨of_add_mul_left_right, fun h ↦ h.add_mul_left_right z⟩

Premises used: IsRelPrime.add_mul_left_right, IsRelPrime.of_add_mul_left_right, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (y + z * x) ↔ IsRelPrime x y

Tactic:
⟨of_add_mul_right_right, fun h ↦ h.add_mul_right_right z⟩

Premises used: IsRelPrime.add_mul_right_right, IsRelPrime.of_add_mul_right_right, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (y * z + x) y ↔ IsRelPrime x y

Tactic:
⟨of_mul_add_left_left, fun h ↦ h.mul_add_left_left z⟩

Premises used: IsRelPrime.mul_add_left_left, IsRelPrime.of_mul_add_left_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime (z * y + x) y ↔ IsRelPrime x y

Tactic:
⟨of_mul_add_right_left, fun h ↦ h.mul_add_right_left z⟩

Premises used: IsRelPrime.of_mul_add_right_left, IsRelPrime.mul_add_right_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (x * z + y) ↔ IsRelPrime x y

Tactic:
⟨of_mul_add_left_right, fun h ↦ h.mul_add_left_right z⟩

Premises used: IsRelPrime.mul_add_left_right, Iff.intro, IsRelPrime.of_mul_add_left_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
⊢ IsRelPrime x (z * x + y) ↔ IsRelPrime x y

Tactic:
⟨of_mul_add_right_right, fun h ↦ h.mul_add_right_right z⟩

Premises used: IsRelPrime.of_mul_add_right_right, IsRelPrime.mul_add_right_right, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
⊢ IsRelPrime (-x) y

Tactic:
fun _ ↦ (h <| dvd_neg.mp ·)

Premises used: IsRelPrime, dvd_neg, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
⊢ IsRelPrime x (-y)

Tactic:
h.symm.neg_left.symm

Premises used: IsRelPrime.neg_left, IsRelPrime.symm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : IsRelPrime x y
⊢ IsRelPrime (-x) (-y)

Tactic:
h.neg_left.neg_right

Premises used: IsRelPrime.neg_left, IsRelPrime.neg_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ IsRelPrime (-x) y ↔ IsRelPrime x y

Tactic:
⟨fun h ↦ neg_neg x ▸ h.neg_left, neg_left⟩

Premises used: IsRelPrime.neg_left, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ IsRelPrime x (-y) ↔ IsRelPrime x y

Tactic:
⟨fun h ↦ neg_neg y ▸ h.neg_right, neg_right⟩

Premises used: IsRelPrime.neg_right, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
⊢ IsRelPrime (-x) (-y) ↔ IsRelPrime x y

Tactic:
(neg_left_iff _ _).trans (neg_right_iff _ _)

Premises used: IsRelPrime.neg_left_iff, IsRelPrime.neg_right_iff, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(y * z)) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (x + y * -z) y ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime (x - y * z) y ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, ← mul_neg, add_mul_left_left_iff]

Premises used: sub_eq_add_neg, IsRelPrime.add_mul_left_left_iff, mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (x + -(z * y)) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (x + -z * y) y ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime (x - z * y) y ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, ← neg_mul, add_mul_right_left_iff]

Premises used: sub_eq_add_neg, IsRelPrime.add_mul_right_left_iff, neg_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(x * z)) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (y + x * -z) ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime x (y - x * z) ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, ← mul_neg, add_mul_left_right_iff]

Premises used: sub_eq_add_neg, IsRelPrime.add_mul_left_right_iff, mul_neg
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (y + -(z * x)) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (y + -z * x) ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime x (y - z * x) ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, ← neg_mul, add_mul_right_right_iff]

Premises used: sub_eq_add_neg, neg_mul, IsRelPrime.add_mul_right_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + y * z) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime (y * z - x) y ↔ IsRelPrime x y

Tactic:
rw [sub_eq_neg_add, add_mul_left_left_iff, neg_left_iff]

Premises used: sub_eq_neg_add, IsRelPrime.neg_left_iff, IsRelPrime.add_mul_left_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime (-x + z * y) y ↔ IsRelPrime x y
rw₁ : IsRelPrime (-x) y ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime (z * y - x) y ↔ IsRelPrime x y

Tactic:
rw [sub_eq_neg_add, add_mul_right_left_iff, neg_left_iff]

Premises used: sub_eq_neg_add, IsRelPrime.neg_left_iff, IsRelPrime.add_mul_right_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (x * z + -y) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime x (x * z - y) ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, mul_add_left_right_iff, neg_right_iff]

Premises used: sub_eq_add_neg, IsRelPrime.neg_right_iff, IsRelPrime.mul_add_left_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y z : R
rw : IsRelPrime x (z * x + -y) ↔ IsRelPrime x y
rw₁ : IsRelPrime x (-y) ↔ IsRelPrime x y
rw₂ rw₃ : IsRelPrime x y ↔ IsRelPrime x y
⊢ IsRelPrime x (z * x - y) ↔ IsRelPrime x y

Tactic:
rw [sub_eq_add_neg, mul_add_right_right_iff, neg_right_iff]

Premises used: sub_eq_add_neg, IsRelPrime.neg_right_iff, IsRelPrime.mul_add_right_right_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
obtain : ∀ (z : R), IsRelPrime (y * z + 1) y
⊢ IsRelPrime (x + 1) y

Tactic:
obtain ⟨z, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
y z : R
rw : IsRelPrime 1 y
⊢ IsRelPrime (y * z + 1) y

Tactic:
rw [mul_add_left_left_iff]

Premises used: IsRelPrime.mul_add_left_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
y z : R
⊢ IsRelPrime 1 y

Tactic:
isRelPrime_one_left

Premises used: isRelPrime_one_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
y z : R
⊢ IsRelPrime 1 y

Tactic:
exact isRelPrime_one_left

Premises used: isRelPrime_one_left
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x ∣ y
⊢ IsRelPrime x (y + 1)

Tactic:
isRelPrime_comm.mp (add_one_left_of_dvd h)

Premises used: IsRelPrime.add_one_left_of_dvd, isRelPrime_comm, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
rw : IsRelPrime (-x + 1) y
⊢ IsRelPrime (x - 1) y

Tactic:
rw [← neg_sub, neg_left_iff, sub_eq_neg_add]

Premises used: neg_sub, sub_eq_neg_add, IsRelPrime.neg_left_iff
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (-x + 1) y

Tactic:
add_one_left_of_dvd h.neg_right

Premises used: Dvd.dvd.neg_right, IsRelPrime.add_one_left_of_dvd
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : y ∣ x
⊢ IsRelPrime (-x + 1) y

Tactic:
exact add_one_left_of_dvd h.neg_right

Premises used: Dvd.dvd.neg_right, IsRelPrime.add_one_left_of_dvd
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x y : R
h : x ∣ y
⊢ IsRelPrime x (y - 1)

Tactic:
isRelPrime_comm.mp (sub_one_left_of_dvd h)

Premises used: IsRelPrime.sub_one_left_of_dvd, isRelPrime_comm, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
h : 2 ∣ x
⊢ 2 + (x - 1) = x + 1

Tactic:
ring
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
x : R
h : 2 ∣ x
⊢ IsRelPrime (x + 1) (x - 1)

Tactic:
simpa [show 2 + (x - 1) = x + 1 by ring] using add_mul_left_left (sub_one_right_of_dvd h) 1

Premises used: IsRelPrime.add_mul_left_left, IsRelPrime.sub_one_right_of_dvd, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
haveI :
  ∀ (this : DecidableEq ι),
    Eq.{u_2 + 1} (α := Ideal R) (⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) ⊤ ↔
      (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
⊢ Eq.{u_2 + 1} (α := Ideal R) (⨆ i ∈ t, ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) ⊤ ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤

Tactic:
haveI : DecidableEq ι := Classical.decEq ι
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
t : Finset ι
h : t.Nonempty
I : ι → Ideal R
this : DecidableEq ι
⊢ (∃ (μ : (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 = ⊤

Tactic:
h.cons_induction ?_ ?_

Premises used: Finset.Nonempty.cons_induction
-- Module: Mathlib.RingTheory.Coprime.Ideal
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 = ⊤
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 = ⊤)
⊢ (∃ (μ : (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 = ⊤

Tactic:
refine h.cons_induction ?_ ?_
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
refine_1 :
  ∀ (a : ι),
    ∃ (μ : (i : ι) → ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)), (↑(μ a) : R) = 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 = ⊤

Tactic:
simp only [Finset.sum_singleton, Finset.coe_singleton, Set.pairwise_singleton, iff_true]

Premises used: Finset.coe_singleton, iff_true, Set.pairwise_singleton, Finset.sum_singleton
-- Module: Mathlib.RingTheory.Coprime.Ideal
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

Tactic:
fun a => ⟨fun i => if h : i = a then ⟨1, ?_⟩ else 0, ?_⟩

Premises used: dite, Subtype.mk, Exists.intro, OfNat.ofNat, Eq
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
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 ⋯
                else 0 :
                ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)))
            a) :
        R)
      1
⊢ ∀ (a : ι),
    ∃ (μ : (i : ι) → ↥(⨅ (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, ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a i : ι
h : i = a
⊢ Membership.mem (γ := Submodule R R) (⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j) 1

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
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 ⋯
              else 0 :
              ↥(⨅ (j : ι), ⨅ (_ : Membership.mem (γ := Finset ι) {a} j), ⨅ (_ : j ≠ i), I j)))
          a) :
      R)
    1

Tactic:
simp only [dif_pos, Submodule.coe_mk]

Premises used: Submodule.coe_mk, dif_pos
-- 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 = ⊤
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) ↔
    (↑(Finset.cons a t hat) : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤

Tactic:
rw [Finset.coe_cons,
    Set.pairwise_insert_of_symmetric fun i j (h : I i ⊔ I j = ⊤) ↦ (sup_comm _ _).trans h]

Premises used: Finset.coe_cons, Set.pairwise_insert_of_symmetric, sup_comm, Eq.trans
-- 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 = ⊤
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 = ⊤
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
⊢ (∃ (μ : (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
-- 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μ : Eq.{u_2 + 1} (α := R) (∑ i ∈ Finset.cons a t hat, (↑(μ i) : R)) 1
⊢ (↑(μ a) : R) + ∑ x ∈ t, (↑(μ x) : R) = 1

Tactic:
rw [Finset.sum_cons] at hμ

Premises used: Finset.sum_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
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤

Tactic:
⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩

Premises used: Pi.single, HAdd.hAdd, And.intro, Exists.intro, Iff.mp, 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μ : (↑(μ 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)
refine₃ : ∀ (i : ι), Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ i), I j) (↑(μ i) : R)
⊢ ((↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ (↑t : Set ι), 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⟩
-- 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 ∈ 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μ : (↑(μ 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)
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)
⊢ Membership.mem (γ := Submodule R R) (⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose (p := Membership.mem t) h), I j) (↑(μ a) : R)

Tactic:
rw [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
this : ∀ (i : ι), Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R)
i : ι
⊢ Membership.mem (γ := Ideal R) (⨅ (_ : i ∈ Finset.cons a t hat), ⨅ (_ : i ≠ a), I i) (↑(μ a) : R)

Tactic:
specialize this i