awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : HPow.hPow (α := S⟦X⟧) (mk 1) (HAdd.hAdd (α := ℕ) 0 1) = mk fun (n : ℕ) ↦ (↑((0 + n).choose 0) : S)
succ :
  ∀ (d : ℕ) (hd : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)),
    HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1 + 1) = mk fun (n : ℕ) ↦ (↑((d + 1 + n).choose (d + 1)) : S)
⊢ HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)

Tactic:
induction d with
  | zero => ext; simp
  | succ d hd =>
      ext n
      rw [pow_add, hd, pow_one, mul_comm, coeff_mul]
      simp_rw [coeff_mk, Pi.one_apply, one_mul]
      norm_cast
      rw [Finset.sum_antidiagonal_choose_add, add_right_comm]

Premises used: Pi.one_apply, pow_add, add_right_comm, PowerSeries.coeff_mk, Finset.sum_antidiagonal_choose_add, PowerSeries.coeff_mul, pow_one, mul_comm, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1
rw₁ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
rw₂ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
rw₃ rw₄ : Eq.{u_1 + 1} (α := S⟦X⟧) 1 1
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1

Tactic:
rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mk_one_mul_one_sub_eq_one, one_pow]

Premises used: one_pow, PowerSeries.mk_one_pow_eq_mk_choose_add, mul_pow, PowerSeries.mk_one_mul_one_sub_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
rw : HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * HPow.hPow (α := S⟦X⟧) (mk 1) (d + 1) = 1
rw₁ : (HSub.hSub (α := S⟦X⟧) 1 X * mk 1) ^ (d + 1) = 1
rw₂ : (mk 1 * HSub.hSub (α := S⟦X⟧) 1 X) ^ (d + 1) = 1
rw₃ : HPow.hPow (α := S⟦X⟧) 1 (d + 1) = 1
rw₄ rw₅ : Eq.{u_1 + 1} (α := S⟦X⟧) 1 1
⊢ (HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) * mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) = 1

Tactic:
rw [← mk_one_pow_eq_mk_choose_add, ← mul_pow, mul_comm, mk_one_mul_one_sub_eq_one, one_pow]

Premises used: one_pow, PowerSeries.mk_one_pow_eq_mk_choose_add, mul_comm, mul_pow, PowerSeries.mk_one_mul_one_sub_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
⊢ Eq.{u_1 + 1} (α := S⟦X⟧ˣ)
    (match (motive := ℕ → S⟦X⟧ˣ) 0 with
      | 0 => 1
      | d.succ =>
        { val := mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1), val_inv := ⋯,
          inv_val := ⋯ } :
      S⟦X⟧ˣ)
    (1 : S⟦X⟧ˣ)

Tactic:
simp only
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
h : 0 < d
rw : (↑(invOneSubPow S (d - 1 + 1)) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
rw₁ :
  (↑{ val := mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d - 1 + 1),
          val_inv := ⋯, inv_val := ⋯ : S⟦X⟧ˣ } :
      S⟦X⟧) =
    mk fun (n : ℕ) ↦ (↑((d - 1 + 1 - 1 + n).choose (d - 1 + 1 - 1)) : S)
rw₂ rw₃ :
  (↑{ val := mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d - 1 + 1),
          val_inv := ⋯, inv_val := ⋯ : S⟦X⟧ˣ } :
      S⟦X⟧) =
    mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)
⊢ (↑(invOneSubPow S d) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d - 1 + n).choose (d - 1)) : S)

Tactic:
rw [← Nat.sub_one_add_one_eq_of_pos h, invOneSubPow, add_tsub_cancel_right]

Premises used: PowerSeries.invOneSubPow, Nat.sub_one_add_one_eq_of_pos, add_tsub_cancel_right
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ (↑(invOneSubPow S (d + 1)) : S⟦X⟧) = mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)

Tactic:
rfl

Premises used: PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
⊢ (↑(invOneSubPow S 1) : S⟦X⟧) = invUnitsSub 1

Tactic:
simp [invOneSubPow, invUnitsSub]

Premises used: PowerSeries.invOneSubPow, PowerSeries.invUnitsSub
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ invOneSubPow S 0 = HPow.hPow (α := S⟦X⟧ˣ) (β := ℕ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ 0

Tactic:
Eq.symm <| pow_zero _

Premises used: pow_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ invOneSubPow S 0 = HPow.hPow (α := S⟦X⟧ˣ) (β := ℕ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ 0

Tactic:
exact Eq.symm <| pow_zero _

Premises used: pow_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
succ :
  invOneSubPow S (d + 1) = (HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) (d + 1))⁻¹
⊢ invOneSubPow S (d + 1) = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ (d + 1)

Tactic:
rw [inv_pow]

Premises used: inv_pow
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
rw :
  (↑(Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) : S⟦X⟧) ^ (d + 1) * (↑(invOneSubPow S (d + 1)) : S⟦X⟧) = 1
⊢ HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) (d + 1) * invOneSubPow S (d + 1) = 1

Tactic:
rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]

Premises used: Units.val_eq_one, Units.val_pow_eq_pow_val, Units.val_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
⊢ (↑(Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) : S⟦X⟧) ^ (d + 1) * (↑(invOneSubPow S (d + 1)) : S⟦X⟧) = 1

Tactic:
(invOneSubPow S (d + 1)).inv_val

Premises used: PowerSeries.invOneSubPow, Units.inv_val, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
⊢ (↑(Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) : S⟦X⟧) ^ (d + 1) * (↑(invOneSubPow S (d + 1)) : S⟦X⟧) = 1

Tactic:
exact (invOneSubPow S (d + 1)).inv_val

Premises used: PowerSeries.invOneSubPow, Units.inv_val, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d
⊢ invOneSubPow S (d + 1) = (HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯) (d + 1))⁻¹

Tactic:
exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
        rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val).symm

Premises used: PowerSeries.invOneSubPow, HAdd.hAdd, OfNat.ofNat, Eq.symm, DivisionMonoid.inv_eq_of_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : invOneSubPow S 0 = HPow.hPow (α := S⟦X⟧ˣ) (β := ℕ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ 0
succ :
  ∀ (d : ℕ),
    invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d →
      invOneSubPow S (d + 1) =
        HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ (d + 1)
⊢ invOneSubPow S d = HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d

Tactic:
induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d _ =>
      rw [inv_pow]
      exact (DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <| by
        rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
        exact (invOneSubPow S (d + 1)).inv_val).symm

Premises used: PowerSeries.invOneSubPow, inv_pow, pow_zero, HAdd.hAdd, OfNat.ofNat, Eq.symm, DivisionMonoid.inv_eq_of_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ Units.inv (invOneSubPow S 0) = HPow.hPow (β := ℕ) (HSub.hSub (α := S⟦X⟧) 1 X) 0

Tactic:
Eq.symm <| pow_zero _

Premises used: pow_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ Units.inv (invOneSubPow S 0) = HPow.hPow (β := ℕ) (HSub.hSub (α := S⟦X⟧) 1 X) 0

Tactic:
exact Eq.symm <| pow_zero _

Premises used: pow_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d_1 d : ℕ
h : Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d
⊢ Units.inv (invOneSubPow S (d + 1)) = HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
zero : Units.inv (invOneSubPow S 0) = HPow.hPow (β := ℕ) (HSub.hSub (α := S⟦X⟧) 1 X) 0
succ :
  ∀ (d : ℕ),
    Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d →
      Units.inv (invOneSubPow S (d + 1)) = HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1)
⊢ Units.inv (invOneSubPow S d) = HSub.hSub (α := S⟦X⟧) 1 X ^ d

Tactic:
induction d with
  | zero => exact Eq.symm <| pow_zero _
  | succ d => rfl

Premises used: pow_zero, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
⊢ Eq.{u_1 + 1} (α := S⟦X⟧)
    (Units.inv
      (match (motive := ℕ → S⟦X⟧ˣ) 0 with
      | 0 => 1
      | d.succ =>
        { val := mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S), inv := HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1), val_inv := ⋯,
          inv_val := ⋯ }))
    1

Tactic:
simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]

Premises used: inv_one, Units.inv_eq_val_inv, Units.val_one
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d : ℕ
⊢ (mk fun (n : ℕ) ↦ (↑((d + n).choose d) : S)) * HSub.hSub (α := S⟦X⟧) 1 X ^ (d + 1) = 1

Tactic:
(invOneSubPow S (d + 1)).val_inv

Premises used: PowerSeries.invOneSubPow, HAdd.hAdd, PowerSeries.mk, OfNat.ofNat, Units.val_inv
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d e : ℕ
simp_rw :
  HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ (d + e) =
    HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ d *
      HPow.hPow (α := S⟦X⟧ˣ) (Units.mkOfMulEqOne (HSub.hSub (α := S⟦X⟧) 1 X) (mk 1) ⋯)⁻¹ e
⊢ invOneSubPow S (d + e) = HMul.hMul (α := S⟦X⟧ˣ) (invOneSubPow S d) (invOneSubPow S e)

Tactic:
simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]

Premises used: pow_add, PowerSeries.invOneSubPow_eq_inv_one_sub_pow
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d e : ℕ
⊢ HSub.hSub (α := S⟦X⟧) 1 X ^ e * (↑(invOneSubPow S (d + e)) : S⟦X⟧) = (↑(invOneSubPow S d) : S⟦X⟧)

Tactic:
simp [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow]

Premises used: PowerSeries.invOneSubPow_inv_eq_one_sub_pow, mul_assoc, PowerSeries.invOneSubPow_add, mul_comm, Units.val_mul
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
S : Type u_1
inst : CommRing S
d e : ℕ
⊢ HSub.hSub (α := S⟦X⟧) 1 X ^ (d + e) * (↑(invOneSubPow S e) : S⟦X⟧) = HSub.hSub (α := S⟦X⟧) 1 X ^ d

Tactic:
simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]

Premises used: PowerSeries.invOneSubPow_inv_eq_one_sub_pow, mul_assoc, pow_add
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (sin A) : A'⟦X⟧) : A')
      ((coeff n : (a : A'⟦X⟧) → A') (sin A') : A')
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (sin A) = sin A'

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (sin A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (sin A') : A')

Tactic:
simp [sin, apply_ite f]

Premises used: PowerSeries.sin, apply_ite, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
h :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (cos A) : A'⟦X⟧) : A')
      ((coeff n : (a : A'⟦X⟧) → A') (cos A') : A')
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (cos A) = cos A'

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.WellKnown
Goal:
A : Type u_1
A' : Type u_2
inst : Ring A
inst_1 : Ring A'
inst_2 : Algebra ℚ A
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (cos A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (cos A') : A')

Tactic:
simp [cos, apply_ite f]

Premises used: apply_ite, PowerSeries.cos, DFunLike.coe
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
x y a : R
hp : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Prime (p i)
hx : x * y = a * ∏ i ∈ ∅, p i
⊢ Eq.{u_2 + 1} (α := Finset α) (∅ ∪ ∅) ∅ ∧
    Disjoint.{u_2} (α := Finset α) ∅ ∅ ∧ a = x * y ∧ x = x * ∏ i ∈ ∅, p i ∧ y = y * ∏ i ∈ ∅, p i

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
x y a : R
hp : ∀ (i : α), Membership.mem (γ := Finset α) ∅ i → Prime (p i)
hx : x * y = a * ∏ i ∈ ∅, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = ∅ ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
exact ⟨∅, ∅, x, y, by simp [hx]⟩
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * ∏ i ∈ insert i s, p i
⊢ x * y = a * p i * ∏ x ∈ s, p x

Tactic:
rw [prod_insert his, ← mul_assoc] at hx

Premises used: Finset.prod_insert, mul_assoc
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
⊢ Prime (p i)

Tactic:
have hpi : Prime (p i) := hp i (mem_insert_self _ _)
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
x y a : R
hp : ∀ i_1 ∈ Insert.insert i s, Prime (p i_1)
hx : x * y = a * p i * ∏ x ∈ s, p x
hpi : Prime (p i)
insert :
  ∀ (t u : Finset α) (b c : R) (htus : t ∪ u = s) (htu : Disjoint t u) (hbc : a * p i = b * c)
    (hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
    ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
      t_1 ∪ u_1 = Insert.insert i s ∧
        Disjoint t_1 u_1 ∧
          a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
⊢ ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
    t ∪ u = Insert.insert i s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i

Tactic:
rcases ih (fun i hi ↦ hp i (mem_insert_of_mem hi)) hx with
      ⟨t, u, b, c, htus, htu, hbc, rfl, rfl⟩

Premises used: Finset.mem_insert_of_mem, rfl
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ i ∉ t

Tactic:
have hit : i ∉ t := fun hit ↦ his (htus ▸ mem_union_left _ hit)
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
⊢ i ∉ u

Tactic:
have hiu : i ∉ u := fun hiu ↦ his (htus ▸ mem_union_right _ hiu)
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
rw : a * p i = p i * a
rw₁ rw₂ : p i * a = p i * a
⊢ b * c = p i * a

Tactic:
rw [← hbc, mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ Insert.insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
b c : R
htus : t ∪ u = s
htu : Disjoint t u
hbc : a * p i = b * c
hx : (b * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hit : i ∉ t
hiu : i ∉ u
insert :
  ∀ (d : R) (hbc : a * p i = p i * d * c) (hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
    ∃ (t_1 : Finset α) (u_1 : Finset α) (b : R) (c_1 : R),
      t_1 ∪ u_1 = Insert.insert i s ∧
        Disjoint t_1 u_1 ∧
          a = b * c_1 ∧ p i * d * ∏ i ∈ t, p i = b * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i
insert₁ :
  ∀ (d : R) (hbc : a * p i = b * (p i * d))
    (hx : (b * ∏ i ∈ t, p i) * (p i * d * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x),
    ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c : R),
      t_1 ∪ u_1 = Insert.insert i s ∧
        Disjoint t_1 u_1 ∧
          a = b_1 * c ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ p i * d * ∏ i ∈ u, p i = c * ∏ i ∈ u_1, p i
⊢ ∃ (t_1 : Finset α) (u_1 : Finset α) (b_1 : R) (c_1 : R),
    t_1 ∪ u_1 = Insert.insert i s ∧
      Disjoint t_1 u_1 ∧
        a = b_1 * c_1 ∧ b * ∏ i ∈ t, p i = b_1 * ∏ i ∈ t_1, p i ∧ c * ∏ i ∈ u, p i = c_1 * ∏ i ∈ u_1, p i

Tactic:
obtain ⟨d, rfl⟩ | ⟨d, rfl⟩ : p i ∣ b ∨ p i ∣ c := hpi.dvd_or_dvd ⟨a, by rw [← hbc, mul_comm]⟩

Premises used: Prime.dvd_or_dvd, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ a = d * c

Tactic:
rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc

Premises used: mul_assoc, Prime.ne_zero, mul_comm, mul_right_inj'
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a * p i = p i * d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
hbc₁ : a = d * c
⊢ (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x

Tactic:
rw [mul_assoc, mul_comm a, mul_right_inj' hpi.ne_zero] at hbc

Premises used: mul_assoc, Prime.ne_zero, mul_comm, mul_right_inj'
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
rw : insert i (t ∪ u) = insert i s
rw₁ rw₂ : insert i s = insert i s
⊢ insert i t ∪ u = insert i s

Tactic:
rw [insert_union, htus]

Premises used: Finset.insert_union
-- Module: Mathlib.RingTheory.Prime
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
α : Type u_2
inst_2 : DecidableEq α
p : α → R
i : α
s : Finset α
his : i ∉ s
ih :
  ∀ {x y a : R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * ∏ i ∈ s, p i),
    ∃ (t : Finset α) (u : Finset α) (b : R) (c : R),
      t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
a : R
hp : ∀ i_1 ∈ insert i s, Prime (p i_1)
hpi : Prime (p i)
t u : Finset α
c : R
htus : t ∪ u = s
htu : Disjoint t u
hit : i ∉ t
hiu : i ∉ u
d : R
hbc : a = d * c
hx : (p i * d * ∏ i ∈ t, p i) * (c * ∏ i ∈ u, p i) = a * p i * ∏ x ∈ s, p x
⊢ a = d * c ∧ p i * d * ∏ i ∈ t, p i = d * ∏ i ∈ insert i t, p i ∧ c * ∏ i ∈ u, p i = c * ∏ i ∈ u, p i

Tactic:
simp [hbc, prod_insert hit, mul_comm, mul_left_comm]

Premises used: Finset.prod_insert, mul_left_comm, mul_comm