-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem Finset.prod_dvd_of_isRelPrime :
    (t : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → (∏ x ∈ t, s x) ∣ z

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
hir : a ∈ r
⊢ False

Tactic:
exact har hir

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ ↑r ⊆ ↑(insert a r)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
i : I
hir : i ∈ r
⊢ a ≠ i

Tactic:
rintro rfl

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
hir : a ∈ r
⊢ False

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z

Tactic:
have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ s a * ∏ x ∈ r, s x ∣ z

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ (↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z

Tactic:
classical
exact Finset.induction_on t (fun _ _ ↦ one_dvd z)
  (by
    intro a r har ih Hs Hs1
    rw [Finset.prod_insert har]
    have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
    refine
      (IsRelPrime.prod_right fun i hir ↦
            Hs aux1 (Finset.mem_insert_of_mem hir) <| by
              rintro rfl
              exact har hir).mul_dvd
        (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
    simp only [Finset.coe_insert, Set.subset_insert])

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ (↑t).Pairwise (IsRelPrime on s) → (∀ i ∈ t, s i ∣ z) → ∏ x ∈ t, s x ∣ z

Tactic:
exact Finset.induction_on t (fun _ _ ↦ one_dvd z)
  (by
    intro a r har ih Hs Hs1
    rw [Finset.prod_insert har]
    have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
    refine
      (IsRelPrime.prod_right fun i hir ↦
            Hs aux1 (Finset.mem_insert_of_mem hir) <| by
              rintro rfl
              exact har hir).mul_dvd
        (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)
    simp only [Finset.coe_insert, Set.subset_insert])

Result:
no goals

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ s a * ∏ x ∈ r, s x ∣ z

Tactic:
refine
  (IsRelPrime.prod_right fun i hir ↦
        Hs aux1 (Finset.mem_insert_of_mem hir) <| by
          rintro rfl
          exact har hir).mul_dvd
    (Hs1 a aux1) (ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi)

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ ↑(insert a r)
⊢ ↑r ⊆ ↑(insert a r)

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ insert a r, s x ∣ z

Tactic:
rw [Finset.prod_insert har]

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z

Proof state:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ ∀ ⦃a : I⦄ {s_1 : Finset I},
    a ∉ s_1 →
      ((↑s_1).Pairwise (IsRelPrime on s) → (∀ i ∈ s_1, s i ∣ z) → ∏ x ∈ s_1, s x ∣ z) →
        (↑(insert a s_1)).Pairwise (IsRelPrime on s) → (∀ i ∈ insert a s_1, s i ∣ z) → ∏ x ∈ insert a s_1, s x ∣ z

Tactic:
intro a r har ih Hs Hs1

Result:
α : Type u_2
I : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ insert a r, s x ∣ z