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 : Finset I
inst_1 : DecidableEq I
h : t.Nonempty
⊢ (∃ (μ : 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))
have singleton : ∀ (a : I),
  (∃ (μ : I → R), Eq.{u + 1} (α := R) (∑ i ∈ {a}, μ i * ∏ j ∈ {a} \ {i}, s j) 1) ↔
    Pairwise.{v} (α := ↥{a}) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥{a}) ↦ s (↑i : I))
Tactic: induction h using Finset.Nonempty.cons_induction with
  | singleton =>
    simp [exists_apply_eq, Pairwise, Function.onFun]
  | cons a t hat h ih =>
    rw [pairwise_cons']
    have mem : ∀ x ∈ t, a ∈ insert a t \ {x} := fun x hx ↦ by
      rw [mem_sdiff, mem_singleton]
      exact ⟨mem_insert_self _ _, fun ha ↦ hat (ha ▸ hx)⟩
    constructor
    · rintro ⟨μ, hμ⟩
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat] at hμ
      refine ⟨ih.mp ⟨Pi.single h.choose (μ a * s h.choose) + μ * fun _ ↦ s a, ?_⟩, fun b hb ↦ ?_⟩
      · rw [prod_eq_mul_prod_diff_singleton_of_mem h.choose_spec, ← mul_assoc, ←
          @if_pos _ _ h.choose_spec R (_ * _) 0, ← sum_pi_single', ← sum_add_distrib] at hμ
        rw [← hμ, sum_congr rfl]
        intro x hx
        convert! add_mul (R := R) _ _ _ using 2
        · by_cases hx : x = h.choose
          · rw [hx, Pi.single_eq_same, Pi.single_eq_same]
          · rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]
        · convert! (mul_assoc _ _ _).symm
          rw [prod_eq_prod_diff_singleton_mul (mem x hx), mul_comm, sdiff_sdiff_comm,
            sdiff_singleton_eq_erase a, erase_insert hat]
      · have : IsCoprime (s b) (s a) :=
          ⟨μ a * ∏ i ∈ t \ {b}, s i, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j, ?_⟩
        · exact ⟨this.symm, this⟩
        rw [mul_assoc, ← prod_eq_prod_diff_singleton_mul hb, sum_mul, ← hμ, sum_congr rfl]
        intro x hx
        rw [mul_assoc]
        congr
        rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
        congr 2
        rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
    · rintro ⟨hs, Hb⟩
      obtain ⟨μ, hμ⟩ := ih.mpr hs
      obtain ⟨u, v, huv⟩ := IsCoprime.prod_left fun b hb ↦ (Hb b hb).right
      use fun i ↦ if i = a then u else v * μ i
      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]
      rw [sum_cons, cons_eq_insert, sdiff_singleton_eq_erase, erase_insert hat]
      simp only [↓reduceIte, ite_mul]
      rw [← huv, ← hμ', sum_congr rfl]
      intro x hx
      rw [mul_assoc, if_neg fun ha : x = a ↦ hat (ha.casesOn hx)]
      rw [mul_assoc]
      congr
      rw [prod_eq_prod_diff_singleton_mul (mem x hx) _]
      congr 2
      rw [sdiff_sdiff_comm, sdiff_singleton_eq_erase a, erase_insert hat]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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 ∈ {i}ᶜ, s j) 1) ↔ Pairwise (IsCoprime on s)
have h : Pairwise (IsCoprime on s) ↔
  Pairwise.{v} (α := ↥univ) (Function.onFun.{v + 1, u + 1, 1} (β := R) IsCoprime fun (i : ↥univ) ↦ s (↑i : I))
Tactic: convert! exists_sum_eq_one_iff_pairwise_coprime Finset.univ_nonempty (s := s) using 1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
s : I → R
t : Finset I
inst_1 : DecidableEq I
⊢ 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)
have rw : (↑t : Set I).Pairwise (IsCoprime on s) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
Tactic: rw [Finset.pairwise_subtype_iff_pairwise_finset']
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
have 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)
Tactic: refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ (↑t : Set I).Pairwise (IsCoprime on s) ↔ ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)
have refine_2 : ∀ (hp : ∀ i ∈ t, IsCoprime (s i) (∏ j ∈ t \ {i}, s j)), (↑t : Set I).Pairwise (IsCoprime on s)
Tactic: refine ⟨fun hp i hi ↦ IsCoprime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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}
⊢ IsCoprime (s i) (s j)
have hj₁ : j ∈ t ∧ ¬j = i
Tactic: rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ (IsCoprime on s) i j
have refine_2 : j ∈ t \ {i}
Tactic: apply IsCoprime.prod_right_iff.mp (hp i hi)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
H : IsCoprime x y
⊢ IsCoprime (x ^ m) y
have rw : IsCoprime (∏ _x ∈ range m, x) y
Tactic: rw [← Finset.card_range m, ← Finset.prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
n : ℕ
H : IsCoprime x y
⊢ IsCoprime x (y ^ n)
have rw : IsCoprime x (∏ _x ∈ range n, y)
Tactic: rw [← Finset.card_range n, ← Finset.prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
⊢ IsCoprime (x ^ m) y ↔ IsCoprime x y
have refine : ∀ (h : IsCoprime (x ^ m) y), IsCoprime x y
Tactic: refine ⟨fun h ↦ ?_, IsCoprime.pow_left⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
x y : R
m : ℕ
hm : 0 < m
h : IsCoprime (x ^ m) y
⊢ IsCoprime x y
have h₁ : IsCoprime (∏ _x ∈ range m, x) y
Tactic: rw [← Finset.card_range m, ← Finset.prod_const] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
have 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
Tactic: refine Finset.induction_on t (fun _ ↦ isRelPrime_one_left) fun b t hbt ih H ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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 (∏ i ∈ insert b t, s i) x
have rw : IsRelPrime (s b * ∏ x ∈ t, s x) x
Tactic: rw [Finset.prod_insert hbt]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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 ∈ t, s x) x
have H₁ : IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
Tactic: rw [Finset.forall_mem_insert] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ (∀ i ∈ t, IsRelPrime (s i) x) → IsRelPrime (∏ i ∈ t, s i) x
have 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
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)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
α : Type u_1
I : Type u_2
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
have 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
Tactic: refine Finset.induction_on t (iff_of_true isRelPrime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
have rw : IsRelPrime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
Tactic: rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
have rw₁ : IsRelPrime (s b) x ∧ IsRelPrime (∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
Tactic: rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
have rw₂ : (IsRelPrime (s b) x ∧ ∀ i ∈ t, IsRelPrime (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]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ IsRelPrime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsRelPrime (s i) x
have rw₃ : (IsRelPrime (s b) x ∧ ∀ i ∈ t, IsRelPrime (s i) x) ↔ IsRelPrime (s b) x ∧ ∀ x_1 ∈ t, IsRelPrime (s x_1) x
Tactic: rw [Finset.prod_insert hbt, IsRelPrime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
α : Type u_1
I : Type u_2
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x : α
s : I → α
t : Finset I
⊢ IsRelPrime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsRelPrime (s i) x
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ ∏ x ∈ insert a r, s x ∣ z
have rw : s a * ∏ x ∈ r, s x ∣ z
Tactic: rw [Finset.prod_insert har]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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
⊢ s a * ∏ x ∈ r, s x ∣ z
have aux1 : a ∈ (↑(insert a r) : Set I)
Tactic: have aux1 : a ∈ (↑(insert a r) : Set I) := Finset.mem_insert_self a r
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ s a * ∏ x ∈ r, s x ∣ z
have fun : (↑r : Set I) ⊆ (↑(insert a r) : Set I)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
have 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)
Tactic: refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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)
⊢ 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)
have 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))
Tactic: refine ⟨fun hp i hi ↦ IsRelPrime.prod_right_iff.mpr fun j hj ↦ ?_, fun hp ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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}
⊢ IsRelPrime (s i) (s j)
have hj₁ : j ∈ t ∧ ¬j = i
Tactic: rw [Finset.mem_sdiff, Finset.mem_singleton] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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
⊢ IsRelPrime (s i) (s j)
have hj₁ : j ∈ t
Tactic: obtain ⟨hj, ji⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
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
⊢ IsRelPrime (s i) (s j)
have ji : ¬j = i
Tactic: obtain ⟨hj, ji⟩ := hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
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
⊢ 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)
have refine_2 : (↑(Subtype.mk (p := fun (x : I) ↦ x ∈ t) j hj) : I) ∈ t \ {i}
Tactic: apply IsRelPrime.prod_right_iff.mp (hp i hi)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
H : IsRelPrime x y
⊢ IsRelPrime (x ^ m) y
have rw : IsRelPrime (∏ _x ∈ Finset.range m, x) y
Tactic: rw [← Finset.card_range m, ← Finset.prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
n : ℕ
H : IsRelPrime x y
⊢ IsRelPrime x (y ^ n)
have rw : IsRelPrime x (∏ _x ∈ Finset.range n, y)
Tactic: rw [← Finset.card_range n, ← Finset.prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
⊢ IsRelPrime (x ^ m) y ↔ IsRelPrime x y
have refine : ∀ (h : IsRelPrime (x ^ m) y), IsRelPrime x y
Tactic: refine ⟨fun h ↦ ?_, IsRelPrime.pow_left⟩
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (x ^ m) y
⊢ IsRelPrime x y
have h₁ : IsRelPrime (∏ _x ∈ Finset.range m, x) y
Tactic: rw [← Finset.card_range m, ← Finset.prod_const] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuationDef 1 = 1
have rw : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk (Ideal.span {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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ v.intValuationDef 1 = 1
have rw₁ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk ⊤))) : ℤ))) 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]
-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.AdicValuation (goal)
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
⊢ v.intValuationDef 1 = 1
have rw₂ : Eq (α := WithZero (Multiplicative ℤ))
  (exp (-(↑(Associates.count (Associates.mk v.asIdeal) (Associates.factors (Associates.mk 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]