awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u + v = 1
⊢ ∑ x ∈ t,
        (↑(if hi : x = a then
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v ⋯
            else
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1)
                (u * (↑(μ x) : R)) ⋯) :
          R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) x) v ⋯) :
        R) =
    1
have huv₁ : u * 1 + v = 1
Tactic: rw [← mul_one u] at huv
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
⊢ ∑ x ∈ t,
        (↑(if hi : x = a then
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v ⋯
            else
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1)
                (u * (↑(μ x) : R)) ⋯) :
          R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) x) v ⋯) :
        R) =
    1
have refine_2 : ∑ x ∈ t,
      (↑(if hi : x = a then
            Subtype.mk (p := fun (x_1 : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v sorry
          else
            Subtype.mk (p := fun (x_1 : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1)
              (u * (↑(μ x) : R)) sorry) :
        R) +
    (↑(Subtype.mk (p := fun (x : R) ↦
          Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) x) v sorry) :
      R) =
  ∑ i ∈ t, u * (↑(μ i) : R) + v
Tactic: rw [← huv, ← hμ, Finset.mul_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
⊢ ∑ x ∈ t,
        (↑(if hi : x = a then
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v ⋯
            else
              Subtype.mk (p := fun (x_1 : R) ↦
                Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1)
                (u * (↑(μ x) : R)) ⋯) :
          R) +
      (↑(Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ a), I j) x) v ⋯) :
        R) =
    ∑ i ∈ t, u * (↑(μ i) : R) + v
have refine_2 : Eq.{u_2 + 1} (α := R)
  (∑ x ∈ t,
    (↑(if hi : x = a then
          Subtype.mk (p := fun (x_1 : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v sorry
        else
          Subtype.mk (p := fun (x_1 : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) (u * (↑(μ x) : R))
            sorry) :
      R))
  (∑ i ∈ t, u * (↑(μ i) : R))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
⊢ Eq.{u_2 + 1} (α := R)
    (∑ x ∈ t,
      (↑(if hi : x = a then
            Subtype.mk (p := fun (x_1 : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v ⋯
          else
            Subtype.mk (p := fun (x_1 : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1)
              (u * (↑(μ x) : R)) ⋯) :
        R))
    (∑ i ∈ t, u * (↑(μ i) : R))
have refine_2 : ∀ x ∈ t,
  (↑(if hi : x = a then
          Subtype.mk (p := fun (x_1 : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) v sorry
        else
          Subtype.mk (p := fun (x_1 : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ x), I j) x_1) (u * (↑(μ x) : R))
            sorry) :
      R) =
    u * (↑(μ x) : R)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Ideal (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih :
  (∃ (μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)), Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1) ↔
    (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
hs : (↑t : Set ι).Pairwise fun (i j : ι) ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ (↑t : Set ι), a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u : R
hu : u ∈ I a
v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
⊢ (↑(if hi : j = a then
          Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j_1 ∈ Finset.cons a t hat, ⨅ (_ : j_1 ≠ j), I j_1) x) v ⋯
        else
          Subtype.mk (p := fun (x : R) ↦
            Membership.mem (γ := Submodule R R) (⨅ j_1 ∈ Finset.cons a t hat, ⨅ (_ : j_1 ≠ j), I j_1) x)
            (u * (↑(μ j) : R)) ⋯) :
      R) =
    u * (↑(μ j) : R)
have refine_2 : ¬j = a
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n : ℤ
⊢ IsCoprime m n ↔ m.gcd n = 1
have mp : IsCoprime m n → m.gcd n = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n : ℤ
mp : IsCoprime m n → m.gcd n = 1
⊢ IsCoprime m n ↔ m.gcd n = 1
have mpr : m.gcd n = 1 → IsCoprime m n
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n a b : ℤ
h : a * m + b * n = 1
⊢ m.gcd n = 1
have mp : (↑1 : ℤ) = m * a + n * b
Tactic: refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n a b : ℤ
h : a * m + b * n = 1
⊢ (↑1 : ℤ) = m * a + n * b
have mp : (↑1 : ℤ) = a * m + n * b
Tactic: rwa [mul_comm m, mul_comm n, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n a b : ℤ
h : a * m + b * n = 1
mp : (↑1 : ℤ) = a * m + n * b
⊢ (↑1 : ℤ) = m * a + n * b
have mp₁ : (↑1 : ℤ) = a * m + b * n
Tactic: rwa [mul_comm m, mul_comm n, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n a b : ℤ
h : a * m + b * n = 1
mp : (↑1 : ℤ) = a * m + n * b
mp₁ : (↑1 : ℤ) = a * m + b * n
⊢ (↑1 : ℤ) = m * a + n * b
have mp₂ : a * m + b * n = (↑1 : ℤ)
Tactic: rwa [mul_comm m, mul_comm n, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n : ℤ
⊢ m.gcd n = 1 → IsCoprime m n
have mpr : m.gcdA n * m + m.gcdB n * n = 1 → ∃ (a : ℤ) (b : ℤ), a * m + b * n = 1
Tactic: rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n : ℕ
⊢ IsCoprime (R := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m.Coprime n
have rw : Int.gcd (↑m : ℤ) (↑n : ℤ) = 1 ↔ m.Coprime n
Tactic: rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
m n : ℕ
rw : Int.gcd (↑m : ℤ) (↑n : ℤ) = 1 ↔ m.Coprime n
⊢ IsCoprime (R := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m.Coprime n
have rw₁ : m.gcd n = 1 ↔ m.Coprime n
Tactic: rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
⊢ IsCoprime (x.gcdA y) y
have h₁ : x * x.gcdA y + x.gcdB y * y = 1
Tactic: use x, x.gcdB y
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
⊢ x * x.gcdA y + x.gcdB y * y = 1
have h₁ : x * x.gcdA y + y * x.gcdB y = 1
Tactic: rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x * x.gcdA y + y * x.gcdB y = 1
⊢ x * x.gcdA y + x.gcdB y * y = 1
have h₂ : Eq (α := ℤ) (↑(x.gcd y) : ℤ) 1
Tactic: rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x * x.gcdA y + y * x.gcdB y = 1
h₂ : Eq (α := ℤ) (↑(x.gcd y) : ℤ) 1
⊢ x * x.gcdA y + x.gcdB y * y = 1
have h₃ : x.gcd y = 1
Tactic: rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
⊢ IsCoprime (x.gcdB y) x
have h₁ : y * x.gcdB y + x.gcdA y * x = 1
Tactic: use y, x.gcdA y
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
⊢ y * x.gcdB y + x.gcdA y * x = 1
have h₁ : x.gcdA y * x + y * x.gcdB y = 1
Tactic: rwa [add_comm, mul_comm, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x.gcdA y * x + y * x.gcdB y = 1
⊢ y * x.gcdB y + x.gcdA y * x = 1
have h₂ : x * x.gcdA y + y * x.gcdB y = 1
Tactic: rwa [add_comm, mul_comm, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x.gcdA y * x + y * x.gcdB y = 1
h₂ : x * x.gcdA y + y * x.gcdB y = 1
⊢ y * x.gcdB y + x.gcdA y * x = 1
have h₃ : Eq (α := ℤ) (↑(x.gcd y) : ℤ) 1
Tactic: rwa [add_comm, mul_comm, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x.gcdA y * x + y * x.gcdB y = 1
h₂ : x * x.gcdA y + y * x.gcdB y = 1
h₃ : Eq (α := ℤ) (↑(x.gcd y) : ℤ) 1
⊢ y * x.gcdB y + x.gcdA y * x = 1
have h₄ : x.gcd y = 1
Tactic: rwa [add_comm, mul_comm, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : ∀ (h : ∀ i ∈ t, IsCoprime (s i) x), IsCoprime (∏ i ∈ t, s i) x
h : ∀ i ∈ Finset.cons b t hbt, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ Finset.cons b t hbt, s i) x
have cons : IsCoprime (s b * ∏ x ∈ t, s x) x
Tactic: rw [Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (hypothesis)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : ∀ (h : ∀ i ∈ t, IsCoprime (s i) x), IsCoprime (∏ i ∈ t, s i) x
h : ∀ i ∈ Finset.cons b t hbt, IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x
have h₁ : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
Tactic: rw [Finset.forall_mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
h : ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ t, s i) x
have empty : ∀ (h : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → IsCoprime (s i) x), IsCoprime (∏ i ∈ ∅, s i) x
Tactic: induction t using Finset.cons_induction with
  | empty => apply isCoprime_one_left
  | cons b t hbt ih =>
    rw [Finset.prod_cons]
    rw [Finset.forall_mem_cons] at h
    exact h.1.mul_left (ih h.2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
h : ∀ i ∈ t, IsCoprime (s i) x
empty : ∀ (h : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → IsCoprime (s i) x), IsCoprime (∏ i ∈ ∅, s i) x
⊢ IsCoprime (∏ i ∈ t, s i) x
have cons : ∀ (b : I) (t : Finset I) (hbt : b ∉ t) (ih : ∀ (h : ∀ i ∈ t, IsCoprime (s i) x), IsCoprime (∏ i ∈ t, s i) x)
  (h : ∀ i ∈ Finset.cons b t hbt, IsCoprime (s i) x), IsCoprime (∏ i ∈ Finset.cons b t hbt, s i) x
Tactic: induction t using Finset.cons_induction with
  | empty => apply isCoprime_one_left
  | cons b t hbt ih =>
    rw [Finset.prod_cons]
    rw [Finset.forall_mem_cons] at h
    exact h.1.mul_left (ih h.2)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
have refine : ∀ (b : I) (t : Finset I) (hbt : b ∉ t) (ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x),
  IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
Tactic: refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
have rw : IsCoprime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
Tactic: rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
rw : IsCoprime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
have rw₁ : IsCoprime (s b) x ∧ IsCoprime (∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
Tactic: rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
rw : IsCoprime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
rw₁ : IsCoprime (s b) x ∧ IsCoprime (∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
have rw₂ : (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
Tactic: rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t_1 : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
rw : IsCoprime (s b * ∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
rw₁ : IsCoprime (s b) x ∧ IsCoprime (∏ x ∈ t, s x) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
rw₂ : (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
have rw₃ : (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
Tactic: rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x
have refine : ∀ (b : I) (t : Finset I) (hbt : b ∉ t) (ih : IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ t, IsCoprime (s i) x),
  IsCoprime (∏ i ∈ insert b t, s i) x ↔ ∀ i ∈ insert b t, IsCoprime (s i) x
Tactic: classical
  refine Finset.induction_on t (iff_of_true isCoprime_one_left fun _ ↦ by simp) fun b t hbt ih ↦ ?_
  rw [Finset.prod_insert hbt, IsCoprime.mul_left_iff, ih, Finset.forall_mem_insert]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ insert a r, s x ∣ z
have insert : s a * ∏ x ∈ r, s x ∣ z
Tactic: rw [Finset.prod_insert har]
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z
have insert : IsCoprime (s a) (∏ x ∈ r, s x)
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(Insert.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : IsCoprime (s a) (∏ x ∈ r, s x)
⊢ s a * ∏ x ∈ r, s x ∣ z
have insert₁ : s a ∣ z
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(Insert.insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ Insert.insert a r, s i ∣ z
insert : IsCoprime (s a) (∏ x ∈ r, s x)
insert₁ : s a ∣ z
⊢ s a * ∏ x ∈ r, s x ∣ z
have insert₂ : ∏ x ∈ r, s x ∣ z
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ IsCoprime (s a) (∏ x ∈ r, s x)
have insert : ∀ (i : I) (hir : i ∈ r), IsCoprime (s a) (s i)
Tactic: refine IsCoprime.prod_right fun i hir ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z
have insert : (↑r : Set I) ⊆ (↑(insert a r) : Set I)
Tactic: refine 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:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑t : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ t, s i ∣ z
⊢ ∏ x ∈ t, s x ∣ z
have empty : ∀ (Hs : (↑∅ : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → s i ∣ z),
  ∏ x ∈ ∅, s x ∣ z
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert a r har ih =>
    rw [Finset.prod_insert har]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
    · exact Hs1 a (Finset.mem_insert_self a r)
    · refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]
Cleared hypotheses: Hs, Hs1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑t : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ t, s i ∣ z
empty :
  ∀ (Hs : (↑∅ : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → s i ∣ z),
    ∏ x ∈ ∅, s x ∣ z
⊢ ∏ x ∈ t, s x ∣ z
have insert : ∀ (a : I) (r : Finset I) (har : a ∉ r)
  (ih : ∀ (Hs : (↑r : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ r, s i ∣ z), ∏ x ∈ r, s x ∣ z)
  (Hs : (↑(insert a r) : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ i ∈ insert a r, s i ∣ z), ∏ x ∈ insert a r, s x ∣ z
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert a r har ih =>
    rw [Finset.prod_insert har]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
    · exact Hs1 a (Finset.mem_insert_self a r)
    · refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]
Cleared hypotheses: Hs, Hs1
-- Lean 4 proof step from Mathlib.RingTheory.Coprime.Lemmas (goal)
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑t : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ t, s i ∣ z
⊢ ∏ x ∈ t, s x ∣ z
have empty : ∀ (Hs : (↑∅ : Set I).Pairwise (IsCoprime on s)) (Hs1 : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → s i ∣ z),
  ∏ x ∈ ∅, s x ∣ z
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert a r har ih =>
    rw [Finset.prod_insert har]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · refine IsCoprime.prod_right fun i hir ↦ ?_
      exact Hs (by simp) (by simp [hir]) (ne_of_mem_of_not_mem hir har).symm
    · exact Hs1 a (Finset.mem_insert_self a r)
    · refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]
Cleared hypotheses: Hs, Hs1