awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
m_1 : Multiset R
a : R
m : Multiset R
ih : Eq (α := Ideal R) (Multiset.prod (Multiset.map (fun (x : R) ↦ span {x}) m)) (span {m.prod})
⊢ Eq (α := Ideal R) (Multiset.prod (Multiset.map (fun (x : R) ↦ span {x}) (a ::ₘ m))) (span {(a ::ₘ m).prod})

Tactic:
simp only [Multiset.map_cons, Multiset.prod_cons, ih, ← Ideal.span_singleton_mul_span_singleton]

Premises used: Multiset.map_cons, Multiset.prod_cons, Ideal.span_singleton_mul_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) x ↔
      Membership.mem (γ := Ideal R) (span {∏ i ∈ s, I i}) x
⊢ Eq (α := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) (span {∏ i ∈ s, I i})

Tactic:
ext x
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
x : R
h : (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x
⊢ Membership.mem (γ := Ideal R) (s.inf fun (i : ι) ↦ span {I i}) x ↔
    Membership.mem (γ := Ideal R) (span {∏ i ∈ s, I i}) x

Tactic:
simp only [Submodule.mem_finsetInf, Ideal.mem_span_singleton]

Premises used: Submodule.mem_finsetInf, Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
x : R
⊢ (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x

Tactic:
⟨Finset.prod_dvd_of_coprime hI, fun h i hi => (Finset.dvd_prod_of_mem _ hi).trans h⟩

Premises used: Finset.dvd_prod_of_mem, Iff.intro, Finset.prod_dvd_of_coprime, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
I : ι → R
hI : (↑s : Set ι).Pairwise (IsCoprime on I)
x : R
⊢ (∀ i ∈ s, I i ∣ x) ↔ ∏ i ∈ s, I i ∣ x

Tactic:
exact ⟨Finset.prod_dvd_of_coprime hI, fun h i hi => (Finset.dvd_prod_of_mem _ hi).trans h⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
inst_1 : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
hI₁ : (↑Finset.univ : Set ι).Pairwise (Function.onFun IsCoprime I)
⊢ Eq (α := Ideal R) (⨅ (i : ι), span {I i}) (span {∏ i : ι, I i})

Tactic:
rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]

Premises used: Ideal.finset_inf_span_singleton, Finset.inf_univ_eq_iInf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
inst_1 : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
hI₁ : Set.Pairwise Set.univ (Function.onFun IsCoprime I)
hI₂ hI₃ hI₄ hI₅ : Pairwise (Function.onFun IsCoprime I)
⊢ (↑Finset.univ : Set ι).Pairwise (Function.onFun IsCoprime I)

Tactic:
rwa [Finset.coe_univ, Set.pairwise_univ]

Premises used: Finset.coe_univ, Set.pairwise_univ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Fintype ι
I : ι → ℕ
hI : Pairwise fun (i j : ι) ↦ (I i).Coprime (I j)
rw : ∀ (i j : ι), i ≠ j → IsCoprime.{u_2} (R := R) (↑(I i) : R) (↑(I j) : R)
⊢ Eq (α := Ideal R) (⨅ (i : ι), span {(↑(I i) : R)}) (span {(↑(∏ i : ι, I i) : R)})

Tactic:
rw [iInf_span_singleton, Nat.cast_prod]

Premises used: Nat.cast_prod, Ideal.iInf_span_singleton
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Fintype ι
I : ι → ℕ
hI : Pairwise fun (i j : ι) ↦ (I i).Coprime (I j)
⊢ ∀ (i j : ι), i ≠ j → IsCoprime.{u_2} (R := R) (↑(I i) : R) (↑(I j) : R)

Tactic:
fun i j h ↦ (hI h).cast

Premises used: Nat.Coprime.cast
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommRing R
ι : Type u_3
inst_1 : Fintype ι
I : ι → ℕ
hI : Pairwise fun (i j : ι) ↦ (I i).Coprime (I j)
⊢ ∀ (i j : ι), i ≠ j → IsCoprime.{u_2} (R := R) (↑(I i) : R) (↑(I j) : R)

Tactic:
exact fun i j h ↦ (hI h).cast

Premises used: Nat.Coprime.cast
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
rw :
  (∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1) ↔
    IsCoprime x y
⊢ Eq (α := Ideal R) (span {x} ⊔ span {y}) ⊤ ↔ IsCoprime x y

Tactic:
rw [eq_top_iff_one, Submodule.mem_sup]

Premises used: Ideal.eq_top_iff_one, Submodule.mem_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
mp :
  (∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1) →
    IsCoprime x y
mpr :
  IsCoprime x y →
    ∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1
⊢ (∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1) ↔
    IsCoprime x y

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y u : R
hu : Membership.mem (γ := Submodule R R) (span {x}) u
v : R
hv : Membership.mem (γ := Submodule R R) (span {y}) v
h1 : u + v = 1
mp : ∀ (hu : ∃ (a : R), a * x = u) (v : R) (hv : ∃ (a : R), a * y = v) (h1 : u + v = 1), IsCoprime x y
⊢ IsCoprime x y

Tactic:
rw [mem_span_singleton'] at hu hv

Premises used: Ideal.mem_span_singleton'
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y u : R
hu : ∃ (a : R), a * x = u
v : R
hv : ∃ (a : R), a * y = v
h1 : u + v = 1
⊢ hu.choose (p := fun (a : R) ↦ a * x = u) * x + hv.choose (p := fun (a : R) ↦ a * y = v) * y = 1

Tactic:
rw [← hu.choose_spec, ← hv.choose_spec] at h1

Premises used: Exists.choose_spec
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y u : R
hu : ∃ (a : R), a * x = u
v : R
hv : ∃ (a : R), a * y = v
h1 : hu.choose (p := fun (a : R) ↦ a * x = u) * x + hv.choose (p := fun (a : R) ↦ a * y = v) * y = 1
⊢ IsCoprime x y

Tactic:
⟨_, _, h1⟩

Premises used: Exists.intro, IsCoprime
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y u : R
hu : ∃ (a : R), a * x = u
v : R
hv : ∃ (a : R), a * y = v
h1 : hu.choose (p := fun (a : R) ↦ a * x = u) * x + hv.choose (p := fun (a : R) ↦ a * y = v) * y = 1
⊢ IsCoprime x y

Tactic:
exact ⟨_, _, h1⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
⊢ IsCoprime x y →
    ∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1

Tactic:
fun ⟨u, v, h1⟩ =>
      ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩

Premises used: Iff.mpr, Ideal.mem_span_singleton', HMul.hMul, _private.0.Ideal.sup_eq_top_iff_isCoprime.match_1, Membership.mem, Exists, And, HAdd.hAdd, And.intro, Exists.intro, Ideal.span, Singleton.singleton, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
⊢ IsCoprime x y →
    ∃ (y_1 : R),
      Membership.mem (γ := Submodule R R) (span {x}) y_1 ∧
        ∃ (z : R), Membership.mem (γ := Submodule R R) (span {y}) z ∧ y_1 + z = 1

Tactic:
exact fun ⟨u, v, h1⟩ =>
      ⟨_, mem_span_singleton'.mpr ⟨_, rfl⟩, _, mem_span_singleton'.mpr ⟨_, rfl⟩, h1⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
⊢ s.prod ≤ s.inf

Tactic:
s.induction_on ?_ ?_

Premises used: Multiset.induction_on
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
refine_2 : ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf
⊢ s.prod ≤ s.inf

Tactic:
refine s.induction_on ?_ ?_
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
⊢ LE.le.{u} (α := Ideal R) (Multiset.prod 0) ⊤

Tactic:
le_top

Premises used: Set.Mem, le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
⊢ LE.le.{u} (α := Ideal R) (Multiset.prod 0) ⊤

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s_1 : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
refine_2 : a * s.prod ≤ a ⊓ s.inf
⊢ (a ::ₘ s).prod ≤ (a ::ₘ s).inf

Tactic:
rw [Multiset.prod_cons, Multiset.inf_cons]

Premises used: Multiset.prod_cons, Multiset.inf_cons
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s_1 : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf

Tactic:
le_trans mul_le_inf (inf_le_inf le_rfl ih)

Premises used: le_rfl, inf_le_inf, Ideal.mul_le_inf, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s_1 : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : s.prod ≤ s.inf
⊢ a * s.prod ≤ a ⊓ s.inf

Tactic:
exact le_trans mul_le_inf (inf_le_inf le_rfl ih)

Premises used: le_rfl, inf_le_inf, Ideal.mul_le_inf, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
refine_2 refine_2₁ refine_2₂ :
  ∀ (a : Ideal R) (s : Multiset (Ideal R)) (ih : s.prod ≤ s.inf), (a ::ₘ s).prod ≤ (a ::ₘ s).inf
refine_2₃ : ∀ (a : Ideal R) (s : Multiset (Ideal R)) (ih : s.prod ≤ s.inf), a * s.prod ≤ a ⊓ s.inf
⊢ s.prod ≤ s.inf

Tactic:
classical
    refine s.induction_on ?_ ?_
    · rw [Multiset.inf_zero]
      exact le_top
    intro a s ih
    rw [Multiset.prod_cons, Multiset.inf_cons]
    exact le_trans mul_le_inf (inf_le_inf le_rfl ih)

Premises used: Multiset.prod_cons, Multiset.inf_zero, Multiset.inf_cons, le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
f : ι → Ideal R
⊢ s.prod f ≤ s.inf f

Tactic:
multiset_prod_le_inf

Premises used: Set.Mem, Ideal.multiset_prod_le_inf
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ I * J = I ⊓ J

Tactic:
le_antisymm mul_le_inf fun r ⟨hri, hrj⟩ =>
    let ⟨s, hsi, t, htj, hst⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 h)
    mul_one r ▸
      hst ▸
        (mul_add r s t).symm ▸ Ideal.add_mem (I * J) (mul_mem_mul_rev hsi hrj) (mul_mem_mul hri htj)

Premises used: HMul.hMul, _private.0.Ideal.mul_eq_inf_of_coprime.match_2, Membership.mem, Eq.rec, Ideal.add_mem, Ideal.mul_mem_mul, le_antisymm, Ideal.eq_top_iff_one, Max.max, _private.0.Ideal.mul_eq_inf_of_coprime.match_1, Iff.mp, Ideal.mul_le_inf, Ideal.mul_mem_mul_rev, mul_add, Submodule.mem_sup, mul_one, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, I ⊔ J i = ⊤
simp_rw simp_rw₁ : I ⊔ 1 = ⊤
simp_rw₂ : I ⊔ ⊤ = ⊤
⊢ I ⊔ 1 = ⊤

Tactic:
simp_rw [one_eq_top, sup_top_eq]

Premises used: Ideal.one_eq_top, sup_top_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
s : Multiset (Ideal R)
h : ∀ p ∈ s, I ⊔ p = ⊤
⊢ (fun (x : Ideal R) ↦ I ⊔ x = ⊤) 1

Tactic:
simp only [one_eq_top, le_top, sup_of_le_right]

Premises used: Ideal.one_eq_top, sup_of_le_right, le_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
rw : ∀ i ∈ s, I ⊔ J i = ⊤
⊢ (∏ i ∈ s, J i) ⊔ I = ⊤

Tactic:
rw [sup_comm, sup_prod_eq_top]

Premises used: sup_comm, Ideal.sup_prod_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
s : Finset ι
J : ι → Ideal R
h : ∀ i ∈ s, J i ⊔ I = ⊤
i : ι
hi : i ∈ s
rw : J i ⊔ I = ⊤
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ I ⊔ J i = ⊤

Tactic:
rw [sup_comm, h i hi]

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsDomain R
s : Multiset (Ideal R)
⊢ s.prod = ⊥ ↔ ⊥ ∈ s

Tactic:
Multiset.prod_eq_zero_iff

Premises used: Multiset.prod_eq_zero_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) ↔ I ⊔ J = ⊤
⊢ IsCoprime I J ↔ Codisjoint I J

Tactic:
rw [IsCoprime, codisjoint_iff]

Premises used: codisjoint_iff, IsCoprime
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
mp : (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) → I ⊔ J = ⊤
mpr : I ⊔ J = ⊤ → ∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1
⊢ (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) ↔ I ⊔ J = ⊤

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
mp : 1 ∈ I ⊔ J
⊢ I ⊔ J = ⊤

Tactic:
rw [eq_top_iff_one]

Premises used: Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
mp : 1 ∈ x * I + y * J
⊢ 1 ∈ I ⊔ J

Tactic:
apply (show x * I + y * J ≤ I ⊔ J from
      sup_le (mul_le_left.trans le_sup_left) (mul_le_left.trans le_sup_right))

Premises used: le_sup_left, le_sup_right, Ideal.mul_le_left, sup_le, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
mp : Membership.mem (γ := Submodule R R) 1 1
⊢ 1 ∈ x * I + y * J

Tactic:
rw [hxy]
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ Membership.mem (γ := Submodule R R) 1 1

Tactic:
simp only [one_eq_top, Submodule.mem_top]

Premises used: Ideal.one_eq_top, Submodule.mem_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ ∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1

Tactic:
⟨1, 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
mpr : 1 * I + 1 * J = 1
⊢ ∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1

Tactic:
refine ⟨1, 1, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : I ⊔ J = ⊤
⊢ 1 * I + 1 * J = 1

Tactic:
simpa only [one_eq_top, top_mul, Submodule.add_eq_sup]

Premises used: Ideal.one_eq_top, Ideal.top_mul, Submodule.add_eq_sup
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : I.IsMaximal
inst_2 : J.IsMaximal
ne : I ≠ J
rw : IsCoatom I → IsCoatom J → ∀ (ne : I ≠ J), Codisjoint I J
⊢ IsCoprime I J

Tactic:
rw [isCoprime_iff_codisjoint, isMaximal_def] at *

Premises used: Ideal.isCoprime_iff_codisjoint, Ideal.isMaximal_def
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : IsCoatom I
inst_2 : IsCoatom J
ne : I ≠ J
⊢ Codisjoint I J

Tactic:
IsCoatom.codisjoint_of_ne ‹_› ‹_› ne

Premises used: IsCoatom.codisjoint_of_ne
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : IsCoatom I
inst_2 : IsCoatom J
ne : I ≠ J
⊢ Codisjoint I J

Tactic:
exact IsCoatom.codisjoint_of_ne ‹_› ‹_› ne

Premises used: IsCoatom.codisjoint_of_ne
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : Codisjoint I J ↔ I + J = 1
rw₁ : I ⊔ J = ⊤ ↔ I + J = 1
rw₂ : I ⊔ J = ⊤ ↔ I ⊔ J = 1
rw₃ rw₄ : I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
⊢ IsCoprime I J ↔ I + J = 1

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]

Premises used: Ideal.one_eq_top, codisjoint_iff, Ideal.add_eq_sup, Ideal.isCoprime_iff_codisjoint
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : IsCoprime I J ↔ I + J = 1
rw₁ rw₂ : I + J = 1 ↔ I + J = 1
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
rw [← add_eq_one_iff, isCoprime_iff_add]

Premises used: Ideal.add_eq_one_iff, Ideal.isCoprime_iff_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : Codisjoint I J ↔ I ⊔ J = ⊤
rw₁ rw₂ : I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
⊢ IsCoprime I J ↔ I ⊔ J = ⊤

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff]

Premises used: codisjoint_iff, Ideal.isCoprime_iff_codisjoint
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
rw : I ⊔ J = ⊤
⊢ IsCoprime I J

Tactic:
rw [isCoprime_iff_sup_eq]

Premises used: Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
by_contra : ∀ (hIJ : ¬I ⊔ J = ⊤), False
⊢ I ⊔ J = ⊤

Tactic:
by_contra hIJ
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ : ¬I ⊔ J = ⊤
obtain : ∀ (P : Ideal R) (hP : P.IsMaximal) (hIJ : I ⊔ J ≤ P), False
⊢ False

Tactic:
obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ

Premises used: Ideal.exists_le_maximal
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ_1 : ¬I ⊔ J = ⊤
P : Ideal R
hP : P.IsMaximal
hIJ : I ⊔ J ≤ P
⊢ False

Tactic:
h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

Premises used: le_sup_left, le_sup_right, Ideal.IsMaximal.isPrime, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ_1 : ¬I ⊔ J = ⊤
P : Ideal R
hP : P.IsMaximal
hIJ : I ⊔ J ≤ P
⊢ False

Tactic:
exact h P (le_trans le_sup_left hIJ) (le_trans le_sup_right hIJ) hP.isPrime

Premises used: le_sup_left, le_sup_right, Ideal.IsMaximal.isPrime, le_trans
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE
⊢ [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE

Tactic:
rw [← isCoprime_iff_codisjoint, ← isCoprime_iff_add, ← isCoprime_iff_exists,
      ← isCoprime_iff_sup_eq]

Premises used: Ideal.isCoprime_iff_exists, Ideal.isCoprime_iff_add, Ideal.isCoprime_iff_codisjoint, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : IsCoprime I J
⊢ Codisjoint I J

Tactic:
isCoprime_iff_codisjoint.mp h

Premises used: Iff.mp, Ideal.isCoprime_iff_codisjoint
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : IsCoprime I J
⊢ I + J = 1

Tactic:
isCoprime_iff_add.mp h

Premises used: Iff.mp, Ideal.isCoprime_iff_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : IsCoprime I J
⊢ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
isCoprime_iff_exists.mp h

Premises used: Ideal.isCoprime_iff_exists, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : IsCoprime I J
⊢ I ⊔ J = ⊤

Tactic:
isCoprime_iff_sup_eq.mp h

Premises used: Iff.mp, Ideal.isCoprime_iff_sup_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y : R
simp_rw : (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
⊢ IsCoprime (R := Ideal R) (span {x}) (span {y}) ↔ IsCoprime x y

Tactic:
simp_rw [isCoprime_iff_codisjoint, codisjoint_iff, eq_top_iff_one, mem_span_singleton_sup,
    mem_span_singleton]

Premises used: codisjoint_iff, Ideal.mem_span_singleton_sup, Ideal.eq_top_iff_one, Ideal.mem_span_singleton, Ideal.isCoprime_iff_codisjoint
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y : R
mp : (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) → IsCoprime x y
mpr : IsCoprime x y → ∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1
⊢ (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y

Tactic:
⟨a, b, mul_comm b y ▸ e⟩

Premises used: Eq.rec, Exists.intro, mul_comm, Eq.symm, IsCoprime
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y a b : R
e : a * x + y * b = 1
⊢ IsCoprime x y

Tactic:
exact ⟨a, b, mul_comm b y ▸ e⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1

Tactic:
⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩

Premises used: Eq.rec, And.intro, Exists.intro, mul_comm, Eq.symm, rfl
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
x y a b : R
e : a * x + b * y = 1
⊢ ∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1

Tactic:
exact ⟨a, _, ⟨b, rfl⟩, mul_comm y b ▸ e⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
simp : ∀ (hf : ∀ j ∈ s, I + J j = ⊤), I + ⨅ j ∈ s, J j = ⊤
⊢ IsCoprime I (⨅ j ∈ s, J j)

Tactic:
simp only [isCoprime_iff_add, one_eq_top] at hf ⊢

Premises used: Ideal.one_eq_top, Ideal.isCoprime_iff_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = ⊤
⊢ I + ⨅ j ∈ s, J j = ⊤

Tactic:
sup_iInf_eq_top hf

Premises used: Ideal.sup_iInf_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = ⊤
⊢ I + ⨅ j ∈ s, J j = ⊤

Tactic:
exact sup_iInf_eq_top hf

Premises used: Ideal.sup_iInf_eq_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
coprime : IsCoprime I J
⊢ I * J = I ⊓ J

Tactic:
(Ideal.mul_eq_inf_of_coprime coprime.sup_eq)

Premises used: Ideal.mul_eq_inf_of_coprime, IsCoprime.sup_eq
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
coprime : IsCoprime I J
⊢ I ⊓ J = I * J

Tactic:
(Ideal.mul_eq_inf_of_coprime coprime.sup_eq).symm

Premises used: Ideal.mul_eq_inf_of_coprime, IsCoprime.sup_eq, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)

Tactic:
simp