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}
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
rw : v * ∑ i ∈ t, (μ i * ∏ j ∈ t \ {i}, s j) * s a = v * s a
rw₁ : v * ((∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
rw₂ : v * (1 * s a) = v * s a
rw₃ rw₄ : v * s a = v * s a
⊢ ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a

Tactic:
rw [← mul_sum, ← sum_mul, hμ, one_mul]

Premises used: Finset.mul_sum, one_mul, 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}
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₁ :
  ∀ (hμ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a),
    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
⊢ 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

Tactic:
have hμ' : (∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a)) = v * s a := by
        rw [← mul_sum, ← sum_mul, hμ, one_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}
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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
h₁ :
  HMul.hMul (α := R) ((fun (i : I) ↦ if i = a then u else v * μ i) a) (∏ j ∈ t, s j) +
      ∑ x ∈ t, HMul.hMul (α := R) ((fun (i : I) ↦ if i = a then u else v * μ i) x) (∏ j ∈ insert a t \ {x}, s j) =
    1
⊢ 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

Tactic:
rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]

Premises used: Finset.sdiff_singleton_eq_erase, Finset.sum_cons, Finset.erase_insert, Finset.cons_eq_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)
μ : 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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
h₁ :
  (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
⊢ HMul.hMul (α := R) ((fun (i : I) ↦ if i = a then u else v * μ i) a) (∏ j ∈ t, s j) +
      ∑ x ∈ t, HMul.hMul (α := R) ((fun (i : I) ↦ if i = a then u else v * μ i) x) (∏ j ∈ insert a t \ {x}, s j) =
    1

Tactic:
simp only [↓reduceIte, ite_mul]

Premises used: ite_mul, reduceIte
-- 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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
h₁ :
  ∀ x ∈ t,
    (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
      v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
⊢ (u * ∏ j ∈ t, s j +
      ∑ x ∈ t, if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1

Tactic:
rw [← huv, ← hμ', sum_congr rfl]

Premises used: Finset.sum_congr, rfl
-- 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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)
⊢ (if x = a then u * ∏ j ∈ insert a t \ {x}, s j else v * μ x * ∏ j ∈ insert a t \ {x}, s j) =
    v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

Tactic:
rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]

Premises used: mul_assoc, Eq.casesOn, if_neg
-- 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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * (μ x * ((∏ j ∈ t \ {x}, s j) * s a))
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * ((μ x * ∏ j ∈ t \ {x}, s j) * s a)

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}
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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : ∏ j ∈ insert a t \ {x}, s j = (∏ j ∈ t \ {x}, s j) * s a
⊢ v * (μ x * ∏ j ∈ insert a t \ {x}, s j) = v * (μ x * ((∏ j ∈ t \ {x}, s j) * s a))

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}
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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = (∏ j ∈ t \ {x}, s j) * s a
⊢ ∏ j ∈ insert a t \ {x}, s j = (∏ j ∈ t \ {x}, s j) * s a

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}
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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : (insert a t \ {x}) \ {a} = t \ {x}
⊢ (∏ x ∈ (insert a t \ {x}) \ {a}, s x) * s a = (∏ j ∈ t \ {x}, s j) * 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}
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μ' : ∑ i ∈ t, v * ((μ i * ∏ j ∈ t \ {i}, s j) * s a) = v * s a
x : I
hx : x ∈ t
h₁ : (insert a t \ {a}) \ {x} = t \ {x}
h₂ : (insert a t).erase a \ {x} = t \ {x}
h₃ h₄ : t \ {x} = t \ {x}
⊢ (insert a t \ {x}) \ {a} = t \ {x}

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
inst_1 : Fintype I
inst_2 : Nonempty I
inst_3 : DecidableEq I
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i : I, μ i * ∏ j ∈ univ \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥univ) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥univ) ↦ s (↑i : I))

Tactic:
exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s)

Premises used: Finset.univ_nonempty, exists_sum_eq_one_iff_pairwise_coprime
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
inst_1 : Fintype I
inst_2 : Nonempty I
inst_3 : DecidableEq I
h :
  Pairwise (IsCoprime on s) ↔
    Pairwise.{v} (α := ↥univ) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥univ) ↦ s (↑i : I))
⊢ (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i : I, μ i * ∏ j ∈ {i}ᶜ, s j) 1) ↔ Pairwise (IsCoprime on s)

Tactic:
convert! exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1

Premises used: Finset.univ_nonempty, exists_sum_eq_one_iff_pairwise_coprime
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
inst_1 : Fintype I
inst_2 : Nonempty I
inst_3 : DecidableEq I
⊢ Pairwise (IsCoprime on s) ↔
    Pairwise.{v} (α := ↥univ) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥univ) ↦ s (↑i : I))

Tactic:
simp only [pairwise_subtype_iff_pairwise_finset', coe_univ, Set.pairwise_univ]

Premises used: Finset.coe_univ, Set.pairwise_univ, Finset.pairwise_subtype_iff_pairwise_finset'
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
rw : (↑t : Set I).Pairwise (IsCoprime on s) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
⊢ Pairwise.{v} (α := ↥t) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥t) ↦ s (↑i : I)) ↔
    ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
rw [Finset.pairwise_subtype_iff_pairwise_finset']

Premises used: Finset.pairwise_subtype_iff_pairwise_finset'
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
⊢ (↑t : Set I).Pairwise (IsCoprime on s) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩

Premises used: Iff.mpr, IsCoprime.prod_right_iff, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
refine_1 :
  ∀ (hp : (↑t : Set I).Pairwise (IsCoprime on s)) (i : I) (hi : i ∈ t) (j : I) (hj : j ∈ t \ {i}), IsCoprime (s i) (s j)
refine_2 : ∀ (hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)), (↑t : Set I).Pairwise (IsCoprime on s)
⊢ (↑t : Set I).Pairwise (IsCoprime on s) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : (↑t : Set I).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t \ {i}
⊢ j ∈ t ∧ ¬j = i

Tactic:
rw [Finset.mem_sdiff, Finset.mem_singleton] at hj

Premises used: Finset.mem_singleton, Finset.mem_sdiff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : (↑t : Set I).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)

Tactic:
(hp hj.1 hi hj.2).symm

Premises used: IsCoprime.symm, And.right, And.left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : (↑t : Set I).Pairwise (IsCoprime on s)
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ IsCoprime (s i) (s j)

Tactic:
exact (hp hj.1 hi hj.2).symm

Premises used: IsCoprime.symm, And.right, And.left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ (↑t : Set I)
j : I
hj : j ∈ (↑t : Set I)
h : i ≠ j
refine_2 : j ∈ t \ {i}
⊢ (IsCoprime on s) i j

Tactic:
apply IsCoprime.prod_right_iff.mp (hp i hi)

Premises used: IsCoprime.prod_right_iff, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ (↑t : Set I)
j : I
hj : j ∈ (↑t : Set I)
h : i ≠ j
⊢ j ∈ t \ {i}

Tactic:
Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

Premises used: Iff.mpr, Finset.mem_singleton, Finset.mem_sdiff, And.intro, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ (↑t : Set I)
j : I
hj : j ∈ (↑t : Set I)
h : i ≠ j
⊢ j ∈ t \ {i}

Tactic:
exact Finset.mem_sdiff.mpr ⟨hj, fun f ↦ h (Finset.mem_singleton.mp f).symm⟩

Premises used: Iff.mpr, Finset.mem_singleton, Finset.mem_sdiff, And.intro, Iff.mp, Eq.symm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
rw : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime (x ^ m) y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const]

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (∏ _x ∈ range m, x) y

Tactic:
IsCoprime.prod_left fun _ _ ↦ H

Premises used: IsCoprime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (∏ _x ∈ range m, x) y

Tactic:
exact IsCoprime.prod_left fun _ _ ↦ H

Premises used: IsCoprime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
rw : IsCoprime x (∏ _x ∈ range n, y)
⊢ IsCoprime x (y ^ n)

Tactic:
rw [← Finset.card_range n, ← Finset.prod_const]

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x ∈ range n, y)

Tactic:
IsCoprime.prod_right fun _ _ ↦ H

Premises used: IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (∏ _x ∈ range n, y)

Tactic:
exact IsCoprime.prod_right fun _ _ ↦ H

Premises used: IsCoprime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m n : ℕ
H : IsCoprime x y
⊢ IsCoprime (x ^ m) (y ^ n)

Tactic:
H.pow_left.pow_right

Premises used: IsCoprime.pow_left, IsCoprime.pow_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y

Tactic:
⟨fun h ↦ ?_, IsCoprime.pow_left⟩

Premises used: IsCoprime.pow_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
refine : ∀ (h : IsCoprime (x ^ m) y), IsCoprime x y
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y

Tactic:
refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime (∏ _x ∈ range m, x) y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const] at h

Premises used: Finset.card_range, Finset.prod_const
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime x y

Tactic:
h.of_prod_left 0 (Finset.mem_range.mpr hm)

Premises used: Iff.mpr, Finset.mem_range, IsCoprime.of_prod_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (∏ _x ∈ range m, x) y
⊢ IsCoprime x y

Tactic:
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

Premises used: Iff.mpr, Finset.mem_range, IsCoprime.of_prod_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
⊢ IsCoprime x (y ^ m) ↔ IsCoprime x y

Tactic:
isCoprime_comm.trans <| (IsCoprime.pow_left_iff hm).trans <| isCoprime_comm

Premises used: isCoprime_comm, IsCoprime.pow_left_iff, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
inst : CommSemiring R
x y : R
m n : ℕ
hm : 0 < m
hn : 0 < n
⊢ IsCoprime (x ^ m) (y ^ n) ↔ IsCoprime x y

Tactic:
(IsCoprime.pow_left_iff hm).trans <| IsCoprime.pow_right_iff hn

Premises used: IsCoprime.pow_left_iff, IsCoprime.pow_right_iff, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
refine :
  ∀ (b : I) (t : Finset I) (hbt : b ∉ t) (ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x)
    (H : ∀ i ∈ insert b t, IsRelPrime (s i) x), IsRelPrime (∏ i ∈ insert b t, s i) x
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
rw : IsRelPrime (s b * ∏ x ∈ t, s x) x
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x

Tactic:
rw [Finset.prod_insert hbt]

Premises used: Finset.prod_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsRelPrime (s i) x
⊢ IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x

Tactic:
rw [Finset.forall_mem_insert] at H

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
H.1.mul_left (ih H.2)

Premises used: IsRelPrime.mul_left, And.right, And.left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
H : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
⊢ IsRelPrime (s b * ∏ x ∈ t, s x) x

Tactic:
exact H.1.mul_left (ih H.2)

Premises used: IsRelPrime.mul_left, And.right, And.left