awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
hj_1 : j ∈ Finset.cons a t hat
ij : j ≠ i
hj : j ∈ t
⊢ u * (↑(μ i) : R) ∈ I j

Tactic:
mul_mem_left _ _ (this _ hj ij)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this_1 : 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
i : ι
hi : ¬i = a
this : ∀ (i_1 : ι) (i_2 : i_1 ∈ t) (i_3 : i_1 ≠ i), (↑(μ i) : R) ∈ I i_1
j : ι
hj_1 : j ∈ Finset.cons a t hat
ij : j ≠ i
hj : j ∈ t
⊢ u * (↑(μ i) : R) ∈ I j

Tactic:
exact mul_mem_left _ _ (this _ hj ij)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
refine_2 :
  Eq.{u_2 + 1} (α := R)
    (∑ i ∈ Finset.cons a t hat,
      (↑(if hi : i = a then
            Subtype.mk (p := fun (x : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) v ⋯
          else
            Subtype.mk (p := fun (x : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) (u * (↑(μ i) : R))
              ⋯) :
        R))
    1
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i ∈ Finset.cons a t hat,
      (↑((fun (i : ι) ↦
              (if hi : i = a then
                  Subtype.mk (p := fun (x : R) ↦
                    Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) v ⋯
                else
                  Subtype.mk (p := fun (x : R) ↦
                    Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x)
                    (u * (↑(μ i) : R)) ⋯ :
                ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)))
            i) :
        R))
    1

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
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 ⋯
            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
⊢ Eq.{u_2 + 1} (α := R)
    (∑ i ∈ Finset.cons a t hat,
      (↑(if hi : i = a then
            Subtype.mk (p := fun (x : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) v ⋯
          else
            Subtype.mk (p := fun (x : R) ↦
              Membership.mem (γ := Submodule R R) (⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j) x) (u * (↑(μ i) : R))
              ⋯) :
        R))
    1

Tactic:
rw [Finset.sum_cons, dif_pos rfl, add_comm]

Premises used: Finset.sum_cons, dif_pos, add_comm, rfl
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
⊢ u * 1 + v = 1

Tactic:
rw [← mul_one u] at huv

Premises used: mul_one
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
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 ⋯
            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
⊢ ∑ 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

Tactic:
rw [← huv, ← hμ, Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
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 ⋯
          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))
⊢ ∑ 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

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
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 ⋯
          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) =
      u * (↑(μ x) : R)
⊢ 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))

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Coprime.Ideal
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
refine_2 : ¬j = a
⊢ (↑(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)

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
t : Finset ι
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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
hat : j ∉ t
Hb : ∀ b ∈ (↑t : Set ι), j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
⊢ False

Tactic:
hat hj
-- Module: Mathlib.RingTheory.Coprime.Ideal
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
I : ι → Ideal R
this : DecidableEq ι
t : Finset ι
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 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : Eq.{u_2 + 1} (α := R) (∑ i ∈ t, (↑(μ i) : R)) 1
u v : R
hv : Membership.mem (γ := Submodule R R) (⨅ i ∈ t, I i) v
huv : u * 1 + v = 1
j : ι
hj : j ∈ t
hat : j ∉ t
Hb : ∀ b ∈ (↑t : Set ι), j ≠ b → I j ⊔ I b = ⊤
hu : u ∈ I j
⊢ False

Tactic:
exact hat hj
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n : ℤ
mp : IsCoprime m n → m.gcd n = 1
mpr : m.gcd n = 1 → IsCoprime m n
⊢ IsCoprime m n ↔ m.gcd n = 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n a b : ℤ
h : a * m + b * n = 1
⊢ m.gcd n = 1

Tactic:
Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)

Premises used: Iff.mpr, Nat.dvd_one, Int.gcd_dvd_iff, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n a b : ℤ
h : a * m + b * n = 1
mp : (↑1 : ℤ) = m * a + n * b
⊢ m.gcd n = 1

Tactic:
refine Nat.dvd_one.mp (Int.gcd_dvd_iff.mpr ⟨a, b, ?_⟩)

Premises used: Iff.mpr, Nat.dvd_one, Int.gcd_dvd_iff, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n a b : ℤ
h : a * m + b * n = 1
mp : (↑1 : ℤ) = a * m + n * b
mp₁ : (↑1 : ℤ) = a * m + b * n
mp₂ mp₃ mp₄ mp₅ : a * m + b * n = (↑1 : ℤ)
⊢ (↑1 : ℤ) = m * a + n * b

Tactic:
rwa [mul_comm m, mul_comm n, eq_comm]

Premises used: eq_comm, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n : ℤ
mpr : m.gcdA n * m + m.gcdB n * n = 1 → ∃ (a : ℤ) (b : ℤ), a * m + b * n = 1
⊢ m.gcd n = 1 → IsCoprime m n

Tactic:
rw [← Int.ofNat_inj, IsCoprime, Int.gcd_eq_gcd_ab, mul_comm m, mul_comm n, Nat.cast_one]

Premises used: Int.ofNat_inj, mul_comm, Nat.cast_one, Int.gcd_eq_gcd_ab, IsCoprime
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n : ℤ
h : m.gcdA n * m + m.gcdB n * n = 1
⊢ ∃ (a : ℤ) (b : ℤ), a * m + b * n = 1

Tactic:
⟨_, _, h⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n : ℤ
h : m.gcdA n * m + m.gcdB n * n = 1
⊢ ∃ (a : ℤ) (b : ℤ), a * m + b * n = 1

Tactic:
exact ⟨_, _, h⟩
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
m n : ℕ
rw : Int.gcd (↑m : ℤ) (↑n : ℤ) = 1 ↔ m.Coprime n
rw₁ rw₂ : m.gcd n = 1 ↔ m.Coprime n
⊢ IsCoprime (R := ℤ) (↑m : ℤ) (↑n : ℤ) ↔ m.Coprime n

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]

Premises used: Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
x : ℚ
⊢ IsCoprime x.num (↑x.den : ℤ)

Tactic:
x.reduced.cast.of_isCoprime_of_dvd_left Int.dvd_natAbs_self

Premises used: Rat.reduced, Nat.Coprime.cast, IsCoprime.of_isCoprime_of_dvd_left, Int.dvd_natAbs_self
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x * x.gcdA y + x.gcdB y * y = 1
⊢ IsCoprime (x.gcdA y) y

Tactic:
use x, x.gcdB y

Premises used: Int.gcdB
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : x * x.gcdA y + y * x.gcdB y = 1
h₂ : Eq (α := ℤ) (↑(x.gcd y) : ℤ) 1
h₃ : x.gcd y = 1
h₄ h₅ h₆ h₇ : IsCoprime x y
⊢ x * x.gcdA y + x.gcdB y * y = 1

Tactic:
rwa [mul_comm _ y, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]

Premises used: Int.isCoprime_iff_gcd_eq_one, Nat.cast_eq_one, mul_comm, Int.gcd_eq_gcd_ab
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
x y : ℤ
h : IsCoprime x y
h₁ : y * x.gcdB y + x.gcdA y * x = 1
⊢ IsCoprime (x.gcdB y) x

Tactic:
use y, x.gcdA y

Premises used: Int.gcdA
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
h₄ : x.gcd y = 1
h₅ h₆ h₇ h₈ : IsCoprime x y
⊢ y * x.gcdB y + x.gcdA y * x = 1

Tactic:
rwa [add_comm, mul_comm, ← Int.gcd_eq_gcd_ab, Nat.cast_eq_one, ← Int.isCoprime_iff_gcd_eq_one]

Premises used: Int.isCoprime_iff_gcd_eq_one, add_comm, Nat.cast_eq_one, mul_comm, Int.gcd_eq_gcd_ab
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
A : Type u
inst : CommRing A
inst_1 : Nontrivial A
a b : ℕ
h : a.Coprime b
⊢ IsCoprime.{u} (R := A) (↑a : A) (↑b : A)

Tactic:
simpa only [map_natCast] using IsCoprime.map (Nat.Coprime.isCoprime h) (Int.castRingHom A)

Premises used: map_natCast, IsCoprime.map, Int.castRingHom, Nat.Coprime.isCoprime
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
h : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ ∅, s i) x

Tactic:
apply isCoprime_one_left

Premises used: isCoprime_one_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
cons : IsCoprime (s b * ∏ x ∈ t, s x) x
⊢ IsCoprime (∏ i ∈ Finset.cons b t hbt, s i) x

Tactic:
rw [Finset.prod_cons]

Premises used: Finset.prod_cons
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x

Tactic:
rw [Finset.forall_mem_cons] at h

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Tactic:
h.1.mul_left (ih h.2)

Premises used: IsCoprime.mul_left, And.right, And.left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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 : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Tactic:
exact h.1.mul_left (ih h.2)

Premises used: IsCoprime.mul_left, And.right, And.left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
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
⊢ IsCoprime (∏ i ∈ t, 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)

Premises used: Finset.forall_mem_cons, Finset.prod_cons, isCoprime_one_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime x (s i)) → IsCoprime x (∏ i ∈ t, s i)

Tactic:
simpa only [isCoprime_comm] using IsCoprime.prod_left (R := R)

Premises used: isCoprime_comm, IsCoprime.prod_left
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
x_1 : I
⊢ Membership.mem (γ := Finset I) ∅ x_1 → IsCoprime (s x_1) x

Tactic:
simp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
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
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ 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 ↦ ?_
-- Module: Mathlib.RingTheory.Coprime.Lemmas
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
rw₃ rw₄ : (IsCoprime (s b) x ∧ ∀ i ∈ t, IsCoprime (s i) x) ↔ IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (∏ i ∈ insert b t, 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]

Premises used: Finset.prod_insert, Finset.forall_mem_insert, IsCoprime.mul_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
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
⊢ IsCoprime (∏ i ∈ t, s i) x ↔ ∀ i ∈ 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]

Premises used: Finset.forall_mem_insert, IsCoprime.mul_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ IsCoprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, IsCoprime x (s i)

Tactic:
simpa only [isCoprime_comm] using IsCoprime.prod_left_iff (R := R)

Premises used: isCoprime_comm, IsCoprime.prod_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
H1 : IsCoprime (∏ i ∈ t, s i) x
i : I
hit : i ∈ t
⊢ IsCoprime (s i) x

Tactic:
IsCoprime.prod_left_iff.1 H1 i hit

Premises used: Iff.mp, IsCoprime.prod_left_iff
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
x : R
s : I → R
t : Finset I
H1 : IsCoprime x (∏ i ∈ t, s i)
i : I
hit : i ∈ t
⊢ IsCoprime x (s i)

Tactic:
IsCoprime.prod_right_iff.1 H1 i hit

Premises used: IsCoprime.prod_right_iff, Iff.mp
-- Module: Mathlib.RingTheory.Coprime.Lemmas
Goal:
R : Type u
I : Type v
inst : CommSemiring R
z : R
s : I → R
t : Finset I
Hs : (↑∅ : Set I).Pairwise (IsCoprime on s)
Hs1 : ∀ (i : I), Membership.mem (γ := Finset I) ∅ i → s i ∣ z
⊢ ∏ x ∈ ∅, s x ∣ z

Tactic:
simp