awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ 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)
have 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)
Tactic: rw [hx, Pi.single_eq_same, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ 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)
have 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
Tactic: rw [hx, Pi.single_eq_same, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ 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)
have 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)
Tactic: rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ 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)
have neg₁ : 0 = HMul.hMul (α := R) 0 (∏ j ∈ t \ {x}, s j)
Tactic: rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ 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)
have neg₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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 * ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (β := I → R) μ (fun (x : I) ↦ s a) x * ∏ j ∈ t \ {x}, s j
have h₁ : ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
Tactic: convert! (mul_assoc _ _ _).symm
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
have 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)
Tactic: rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
have 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)
Tactic: rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
have 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)
Tactic: rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
have 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)
Tactic: rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ ∏ j ∈ insert a t \ {x}, s j = HMul.hMul (α := R) ((fun (x : I) ↦ s a) x) (∏ j ∈ t \ {x}, s j)
have h₅ : s a * ∏ x ∈ t \ {x}, s x = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons : ∀ (this : IsCoprime (s b) (s a)), 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, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ IsCoprime (s a) (s b) ∧ IsCoprime (s b) (s a)
have cons₁ : (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1
Tactic: have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ (μ a * ∏ i ∈ t \ {b}, s i) * s b + (∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j) * s a = 1
have cons : ∀ x ∈ t, (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j
Tactic: rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ (μ x * ∏ j ∈ t \ {x}, s j) * s a = μ x * ∏ j ∈ insert a t \ {x}, s j
have cons : μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ μ x * ((∏ j ∈ t \ {x}, s j) * s a) = μ x * ∏ j ∈ insert a t \ {x}, s j
have cons : (∏ j ∈ t \ {x}, s j) * s a = ∏ j ∈ insert a t \ {x}, s j
Tactic: congr