awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
h₁ :
  Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
h₂ : μ x * ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j
⊢ HAdd.hAdd (α := (j : I) → R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)))
        (μ * fun (x : I) ↦ s a) x *
      ∏ j ∈ t \ {x}, s j =
    HAdd.hAdd (α := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
          x :
        R)
      (μ x * ∏ j ∈ insert a t \ {x}, s j)

Tactic:
convert! add_mul (R := R) _ _ _ using 2

Premises used: add_mul
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
pos :
  ∀ (hx : x = Exists.choose (p := Membership.mem t) h),
    Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
        (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
        x =
      HMul.hMul (α := R) (β := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
          R)
        (∏ j ∈ t \ {x}, s j : R)
neg :
  ∀ (hx : ¬x = Exists.choose (p := Membership.mem t) h),
    Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
        (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
        x =
      HMul.hMul (α := R) (β := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
          R)
        (∏ j ∈ t \ {x}, s j : R)
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)

Tactic:
by_cases hx : x = h.choose

Premises used: Exists.choose
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx_1 : x ∈ t
hx : x = Exists.choose (p := Membership.mem t) h
pos :
  Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
      (Exists.choose (p := Membership.mem t) h) =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) (Exists.choose (p := Membership.mem t) h) :
        R)
      (∏ j ∈ t \ {Exists.choose (p := Membership.mem t) h}, s j : R)
pos₁ :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) (Exists.choose (p := Membership.mem t) h) :
        R)
      (∏ j ∈ t \ {Exists.choose (p := Membership.mem t) h}, s j : R)
pos₂ pos₃ :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x =
    μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ j ∈ t \ {Exists.choose (p := Membership.mem t) h}, s j
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)

Tactic:
rw [hx, Pi.single_eq_same, Pi.single_eq_same]

Premises used: Pi.single_eq_same
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx_1 : x ∈ t
hx : ¬x = Exists.choose (p := Membership.mem t) h
neg :
  0 =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)
neg₁ : 0 = HMul.hMul (α := R) 0 (∏ j ∈ t \ {x}, s j)
neg₂ neg₃ : Eq.{u + 1} (α := R) 0 0
⊢ Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
      (μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x) x =
    HMul.hMul (α := R) (β := R)
      (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
          (μ a * s (Exists.choose (p := Membership.mem t) h)) x :
        R)
      (∏ j ∈ t \ {x}, s j : R)

Tactic:
rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]

Premises used: MulZeroClass.zero_mul, Pi.single_eq_of_ne
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
⊢ μ x * HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j) =
    μ x * (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
(mul_assoc _ _ _).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
h₁ : ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
⊢ μ x * ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j

Tactic:
convert! (mul_assoc _ _ _).symm

Premises used: mul_assoc, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ_1 :
  μ a * s (Exists.choose (p := Membership.mem t) h) * ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x +
      ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j =
    1
hμ :
  Eq.{u + 1} (α := R)
    (∑ x ∈ t,
      HAdd.hAdd (α := R)
        (Pi.single (M := fun (a : I) ↦ R) (Exists.choose (p := Membership.mem t) h)
            (μ a * s (Exists.choose (p := Membership.mem t) h) *
              ∏ x ∈ t \ {Exists.choose (p := Membership.mem t) h}, s x)
            x :
          R)
        (μ x * ∏ j ∈ insert a t \ {x}, s j))
    1
x : I
hx : x ∈ t
h₁ : (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
h₂ : s a * ∏ x ∈ (insert a t \ {x}) \ {a}, s x = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
h₃ : s a * ∏ x ∈ (insert a t \ {a}) \ {x}, s x = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
h₄ : s a * ∏ x ∈ (insert a t).erase a \ {x}, s x = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
h₅ h₆ : s a * ∏ x ∈ t \ {x}, s x = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)

Tactic:
rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]

Premises used: Finset.sdiff_singleton_eq_erase, sdiff_sdiff_comm, Finset.prod_eq_prod_diff_singleton_mul, Finset.erase_insert, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
cons : ∀ (this : IsCoprime (s b) (s a)), IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
cons₁ : (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
this : IsCoprime (s b) (s a)
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
⟨this.symm, this⟩

Premises used: IsCoprime.symm, And.intro
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
this : IsCoprime (s b) (s a)
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)

Tactic:
exact ⟨this.symm, this⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
cons : ∀ x ∈ t, (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j
⊢ (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1

Tactic:
rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]

Premises used: mul_assoc, Finset.prod_eq_prod_diff_singleton_mul, Finset.sum_congr, rfl, Finset.sum_mul
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
cons : μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j
⊢ (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
cons : (∏ j ∈ t \ {x}, s j) * s a = ∏ j ∈ insert a t \ {x}, s j
⊢ μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j

Tactic:
congr
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
cons : (∏ j ∈ t \ {x}, s j) * s a = (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a
⊢ (∏ j ∈ t \ {x}, s j) * s a = ∏ j ∈ insert a t \ {x}, s j

Tactic:
rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]

Premises used: Finset.prod_eq_prod_diff_singleton_mul
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
cons : t \ {x} = (insert a t \ {x}) \ {a}
⊢ (∏ j ∈ t \ {x}, s j) * s a = (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a

Tactic:
congr 2
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ : μ a * ∏ j ∈ t, s j + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
b : I
hb : b ∈ t
x : I
hx : x ∈ t
cons : t \ {x} = (insert a t \ {a}) \ {x}
cons₁ : t \ {x} = (insert a t).erase a \ {x}
cons₂ cons₃ : t \ {x} = t \ {x}
⊢ t \ {x} = (insert a t \ {x}) \ {a}

Tactic:
rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]

Premises used: Finset.sdiff_singleton_eq_erase, sdiff_sdiff_comm, Finset.erase_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I))
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
cons :
  ∀ (μ : I → R) (hμ : Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1),
    ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1
⊢ ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1

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

Premises used: Iff.mpr
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I))
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1
cons :
  ∀ (u v : R) (huv : u * ∏ i ∈ t, s i + v * s a = 1),
    ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1
⊢ ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ Finset.cons a t hat, μ i * ∏ j ∈ Finset.cons a t hat \ {i}, s j) 1

Tactic:
obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right

Premises used: And.right, IsCoprime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t_1 : Finset I
inst_1 : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I))
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
hs : Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (a : ↥t) ↦ s (↑a : I))
Hb : ∀ b ∈ t, IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
μ : I → R
hμ : Eq.{u + 1} (α := R) (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) 1
u v : R
huv : u * ∏ i ∈ t, s i + v * s a = 1
h₁ :
  Eq.{u + 1} (α := R)
    (∑ i ∈ cons a t hat,
      HMul.hMul (α := R) ((fun (i : I) ↦ if i = a then u else v * μ i) i) (∏ j ∈ cons a t hat \ {i}, s j))
    1
⊢ ∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ cons a t hat, μ i * ∏ j ∈ cons a t hat \ {i}, s j) 1

Tactic:
use fun i ↦ if i = a then u else v * μ i

Premises used: HMul.hMul, Eq, ite