awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 (s b * ∏ x ∈ t, s x) x
refine₂ :
  ∀ (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
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x

Tactic:
classical
  refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
  rw [Finset.prod_insert hbt]
  rw [Finset.forall_mem_insert] at H
  exact H.1.mul_left (ih H.2)

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 : Finset I
⊢ (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)

Tactic:
simpa only [isRelPrime_comm] using IsRelPrime.prod_left (α := α)

Premises used: IsRelPrime.prod_left, isRelPrime_comm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
I : Type u_2
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
x_1 : I
⊢ Membership.mem (γ := Finset I) ∅ x_1 → IsRelPrime (s x_1) x

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

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

Tactic:
rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

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

Tactic:
classical
  refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]

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

Tactic:
simpa only [isRelPrime_comm] using IsRelPrime.prod_left_iff (α := α)

Premises used: isRelPrime_comm, IsRelPrime.prod_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
I : Type u_2
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
H1 : IsRelPrime (∏ i ∈ t, s i) x
i : I
hit : i ∈ t
⊢ IsRelPrime (s i) x

Tactic:
IsRelPrime.prod_left_iff.1 H1 i hit

Premises used: Iff.mp, IsRelPrime.prod_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
I : Type u_2
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
H1 : IsRelPrime x (∏ i ∈ t, s i)
i : I
hit : i ∈ t
⊢ IsRelPrime x (s i)

Tactic:
IsRelPrime.prod_right_iff.1 H1 i hit

Premises used: Iff.mp, IsRelPrime.prod_right_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
rw : s a * ∏ x ∈ r, s x ∣ z
⊢ ∏ x ∈ insert a r, s x ∣ z

Tactic:
rw [Finset.prod_insert har]

Premises used: Finset.prod_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ a ∈ (↑(insert a r) : Set I)

Tactic:
have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ (↑(insert a r) : Set I)
hir : a ∈ r
⊢ False

Tactic:
har hir
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ (↑(insert a r) : Set I)
hir : a ∈ r
⊢ False

Tactic:
exact har hir
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ (↑(insert a r) : Set I)
fun : (↑r : Set I) ⊆ (↑(insert a r) : Set I)
⊢ 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)

Premises used: Set.Pairwise.mono, IsRelPrime.mul_dvd, IsRelPrime.prod_right, Finset.mem_insert_of_mem
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r : Set I).Pairwise (IsRelPrime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsRelPrime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
aux1 : a ∈ (↑(insert a r) : Set I)
⊢ (↑r : Set I) ⊆ (↑(insert a r) : Set I)

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

Premises used: Finset.coe_insert, Set.subset_insert
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ (↑t : Set I).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])
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
t : Finset I
⊢ (↑t : Set I).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])
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
z : α
s : I → α
inst_2 : Fintype I
Hs : Pairwise (IsRelPrime on s)
Hs1 : ∀ (i : I), s i ∣ z
⊢ ∏ x : I, s x ∣ z

Tactic:
Finset.prod_dvd_of_isRelPrime (Hs.set_pairwise _) fun i _ ↦ Hs1 i

Premises used: Finset.prod_dvd_of_isRelPrime, Pairwise.set_pairwise
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
⊢ Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I)) ↔
    ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)

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

Premises used: Iff.mpr, Iff.intro, IsRelPrime.prod_right_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
refine_1 :
  ∀ (hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I)))
    (i : I) (hi : i ∈ t) (j : I) (hj : j ∈ t \ {i}), IsRelPrime (s i) (s j)
refine_2 :
  ∀ (hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)),
    Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
⊢ Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I)) ↔
    ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)

Tactic:
refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
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:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
⊢ j ∈ t

Tactic:
obtain ⟨hj, ji⟩ := hj
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
i : I
hi : i ∈ t
j : I
hj : j ∈ t ∧ ¬j = i
hj₁ : j ∈ t
⊢ ¬j = i

Tactic:
obtain ⟨hj, ji⟩ := hj
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsRelPrime (s i) (s j)

Tactic:
@hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm

Premises used: congrArg, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : Pairwise.{u_1} (α := ↥t) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime fun (i : ↥t) ↦ s (↑i : I))
i : I
hi : i ∈ t
j : I
hj : j ∈ t
ji : ¬j = i
⊢ IsRelPrime (s i) (s j)

Tactic:
exact @hp ⟨i, hi⟩ ⟨j, hj⟩ fun h ↦ ji (congrArg Subtype.val h).symm

Premises used: congrArg, Eq.symm, Subtype.val
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : Subtype.mk (p := fun (x : I) ↦ x ∈ t) i hi ≠ Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj
refine_2 : (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj) : I) ∈ t \ {i}
⊢ Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := α) IsRelPrime (fun (i : ↥t) ↦ s (↑i : I))
    (Subtype.mk (p := fun (x : I) ↦ x ∈ t) i hi) (Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj)

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

Premises used: Iff.mp, IsRelPrime.prod_right_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_2
I : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
s : I → α
t : Finset I
inst_2 : DecidableEq I
hp : ∀ i ∈ t, IsRelPrime (s i) (∏ j ∈ t \ {i}, s j)
i : I
hi : i ∈ t
j : I
hj : j ∈ t
h : Subtype.mk (p := fun (x : I) ↦ x ∈ t) i hi ≠ Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj
⊢ (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj) : I) ∈ t \ {i}

Tactic:
grind
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
rw : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime (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:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (∏ _x ∈ Finset.range m, x) y

Tactic:
IsRelPrime.prod_left fun _ _ ↦ H

Premises used: IsRelPrime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (∏ _x ∈ Finset.range m, x) y

Tactic:
exact IsRelPrime.prod_left fun _ _ ↦ H

Premises used: IsRelPrime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
rw : IsRelPrime x (∏ _x ∈ Finset.range n, y)
⊢ IsRelPrime 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:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (∏ _x ∈ Finset.range n, y)

Tactic:
IsRelPrime.prod_right fun _ _ ↦ H

Premises used: IsRelPrime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (∏ _x ∈ Finset.range n, y)

Tactic:
exact IsRelPrime.prod_right fun _ _ ↦ H

Premises used: IsRelPrime.prod_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (x ^ m) (y ^ n)

Tactic:
H.pow_left.pow_right

Premises used: IsRelPrime.pow_left, IsRelPrime.pow_right
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
⊢ IsRelPrime (x ^ m) y ↔ IsRelPrime x y

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

Premises used: IsRelPrime.pow_left, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
refine : ∀ (h : IsRelPrime (x ^ m) y), IsRelPrime x y
⊢ IsRelPrime (x ^ m) y ↔ IsRelPrime x y

Tactic:
refine ⟨fun h ↦ ?_, IsRelPrime.pow_left⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (x ^ m) y
⊢ IsRelPrime (∏ _x ∈ Finset.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:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime x y

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

Premises used: Iff.mpr, Finset.mem_range, IsRelPrime.of_prod_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime x y

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

Premises used: Iff.mpr, Finset.mem_range, IsRelPrime.of_prod_left, OfNat.ofNat
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
⊢ IsRelPrime x (y ^ m) ↔ IsRelPrime x y

Tactic:
isRelPrime_comm.trans <| (IsRelPrime.pow_left_iff hm).trans <| isRelPrime_comm

Premises used: IsRelPrime.pow_left_iff, isRelPrime_comm, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m n : ℕ
hm : 0 < m
hn : 0 < n
⊢ IsRelPrime (x ^ m) (y ^ n) ↔ IsRelPrime x y

Tactic:
(IsRelPrime.pow_left_iff hm).trans (IsRelPrime.pow_right_iff hn)

Premises used: IsRelPrime.pow_right_iff, IsRelPrime.pow_left_iff, Iff.trans
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r = 0
⊢ v.intValuationDef r = 0

Tactic:
if_pos hr

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef, if_pos
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 0 = 0

Tactic:
if_pos rfl

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef, if_pos, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
⊢ v.intValuationDef r =
    exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {r})))) : ℤ))

Tactic:
if_neg hr

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef, if_neg
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 0 = 0

Tactic:
v.intValuationDef_if_pos rfl

Premises used: IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos, rfl
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
rw₈ rw₉ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
⊢ v.intValuationDef 1 = 1

Tactic:
rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]

Premises used: Ideal.one_eq_top, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, Ideal.span_singleton_one, Associates.count_zero, Associates.mk_one, Int.ofNat_zero, one_ne_zero, neg_zero, Associates.factors_one, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, WithZero.exp_zero
-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
rw :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {1})))) : ℤ))) 1
rw₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 1
rw₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 1))) : ℤ))) 1
rw₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors 1)) : ℤ))) 1
rw₄ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑(Associates.count (Associates.mk v.asIdeal) 0) : ℤ))) 1
rw₅ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-(↑0 : ℤ))) 1
rw₆ : Eq (α := WithZero (Multiplicative ℤ)) (exp (-0)) 1
rw₇ : Eq (α := WithZero (Multiplicative ℤ)) (exp 0) 1
rw₈ rw₉ : Eq (α := WithZero (Multiplicative ℤ)) 1 1
⊢ v.intValuationDef 1 = 1

Tactic:
classical
  rw [v.intValuationDef_if_neg one_ne_zero, Ideal.span_singleton_one, ← Ideal.one_eq_top,
    Associates.mk_one, Associates.factors_one, Associates.count_zero v.associates_irreducible,
    Int.ofNat_zero, neg_zero, exp_zero]

Premises used: Ideal.one_eq_top, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, Ideal.span_singleton_one, Associates.count_zero, Associates.mk_one, Int.ofNat_zero, one_ne_zero, neg_zero, Associates.factors_one, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, WithZero.exp_zero