awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ Eq (α := Ideal R) (⨅ (i : ι), span {I i}) (span {∏ i : ι, I i})
have hI₁ : (↑Finset.univ : Set ι).Pairwise (Function.onFun IsCoprime I)
Tactic: rw [← Finset.inf_univ_eq_iInf, finset_inf_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ (↑Finset.univ : Set ι).Pairwise (Function.onFun IsCoprime I)
have hI₁ : Set.Pairwise Set.univ (Function.onFun IsCoprime I)
Tactic: rwa [Finset.coe_univ, Set.pairwise_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ (↑Finset.univ : Set ι).Pairwise (Function.onFun IsCoprime I)
have hI₂ : Pairwise (Function.onFun IsCoprime I)
Tactic: rwa [Finset.coe_univ, Set.pairwise_univ]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ Eq (α := Ideal R) (⨅ (i : ι), span {(↑(I i) : R)}) (span {(↑(∏ i : ι, I i) : R)})
have rw : ∀ (i j : ι), i ≠ j → IsCoprime.{u_2} (R := R) (↑(I i) : R) (↑(I j) : R)
Tactic: rw [iInf_span_singleton, Nat.cast_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
⊢ Eq (α := Ideal R) (span {x} ⊔ span {y}) ⊤ ↔ IsCoprime x y
have 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
Tactic: rw [eq_top_iff_one, Submodule.mem_sup]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u_2
inst : CommSemiring R
x y : R
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ IsCoprime x y
have mp : ∀ (hu : ∃ (a : R), a * x = u) (v : R) (hv : ∃ (a : R), a * y = v) (h1 : u + v = 1), IsCoprime x y
Tactic: rw [mem_span_singleton'] at hu hv
Cleared hypotheses: hu, v, hv, h1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
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
⊢ IsCoprime x y
have h1₁ : 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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
⊢ s.prod ≤ s.inf
have refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
⊢ s.prod ≤ s.inf
have refine_2 : ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ s).inf
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have refine_2 : a * s.prod ≤ a ⊓ s.inf
Tactic: rw [Multiset.prod_cons, Multiset.inf_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
⊢ s.prod ≤ s.inf
have refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
s : Multiset (Ideal R)
refine_1 : LE.le.{u} (α := Ideal R) (Multiset.prod 0) (Multiset.inf 0)
⊢ s.prod ≤ s.inf
have refine_2 : ∀ (a : Ideal R) (s : Multiset (Ideal R)), s.prod ≤ s.inf → (a ::ₘ s).prod ≤ (a ::ₘ 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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ s.prod ≤ s.inf
have refine_2₃ : ∀ (a : Ideal R) (s : Multiset (Ideal R)) (ih : s.prod ≤ s.inf), a * s.prod ≤ a ⊓ 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)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ 1 = ⊤
have simp_rw₂ : I ⊔ ⊤ = ⊤
Tactic: simp_rw [one_eq_top, sup_top_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 ∈ s, J i) ⊔ I = ⊤
have rw : ∀ i ∈ s, I ⊔ J i = ⊤
Tactic: rw [sup_comm, sup_prod_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ I ⊔ J i = ⊤
have rw : J i ⊔ I = ⊤
Tactic: rw [sup_comm, h i hi]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ I ⊔ J i = ⊤
have rw₁ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
Tactic: rw [sup_comm, h i hi]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ Codisjoint I J
have rw : (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) ↔ I ⊔ J = ⊤
Tactic: rw [IsCoprime, codisjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) ↔ I ⊔ J = ⊤
have mp : (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) → I ⊔ J = ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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 = ⊤
⊢ (∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1) ↔ I ⊔ J = ⊤
have mpr : I ⊔ J = ⊤ → ∃ (a : Ideal R) (b : Ideal R), a * I + b * J = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ I ⊔ J = ⊤
have mp : 1 ∈ I ⊔ J
Tactic: rw [eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ I ⊔ J
have mp : 1 ∈ x * I + y * 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))
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J x y : Ideal R
hxy : x * I + y * J = 1
⊢ 1 ∈ x * I + y * J
have mp : Membership.mem (γ := Submodule R R) 1 1
Tactic: rw [hxy]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
have mpr : 1 * I + 1 * J = 1
Tactic: refine ⟨1, 1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
inst_1 : I.IsMaximal
inst_2 : J.IsMaximal
ne : I ≠ J
⊢ IsCoprime I J
have rw : IsCoatom I → IsCoatom J → ∀ (ne : I ≠ J), Codisjoint I J
Tactic: rw [isCoprime_iff_codisjoint, isMaximal_def] at *
Cleared hypotheses: inst_1, inst_2, ne
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I + J = 1
have rw : Codisjoint I J ↔ I + J = 1
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : Codisjoint I J ↔ I + J = 1
⊢ IsCoprime I J ↔ I + J = 1
have rw₁ : I ⊔ J = ⊤ ↔ I + J = 1
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : Codisjoint I J ↔ I + J = 1
rw₁ : I ⊔ J = ⊤ ↔ I + J = 1
⊢ IsCoprime I J ↔ I + J = 1
have rw₂ : I ⊔ J = ⊤ ↔ I ⊔ J = 1
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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
⊢ IsCoprime I J ↔ I + J = 1
have rw₃ : I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw : IsCoprime I J ↔ I + J = 1
Tactic: rw [← add_eq_one_iff, isCoprime_iff_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : IsCoprime I J ↔ I + J = 1
⊢ IsCoprime I J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
have rw₁ : I + J = 1 ↔ I + J = 1
Tactic: rw [← add_eq_one_iff, isCoprime_iff_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I ⊔ J = ⊤
have rw : Codisjoint I J ↔ I ⊔ J = ⊤
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
rw : Codisjoint I J ↔ I ⊔ J = ⊤
⊢ IsCoprime I J ↔ I ⊔ J = ⊤
have rw₁ : I ⊔ J = ⊤ ↔ I ⊔ J = ⊤
Tactic: rw [isCoprime_iff_codisjoint, codisjoint_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ IsCoprime I J
have rw : I ⊔ J = ⊤
Tactic: rw [isCoprime_iff_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
⊢ I ⊔ J = ⊤
have by_contra : ∀ (hIJ : ¬I ⊔ J = ⊤), False
Tactic: by_contra hIJ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
h : ∀ (P : Ideal R), I ≤ P → J ≤ P → ¬P.IsPrime
hIJ : ¬I ⊔ J = ⊤
⊢ False
have obtain : ∀ (P : Ideal R) (hP : P.IsMaximal) (hIJ : I ⊔ J ≤ P), False
Tactic: obtain ⟨P, hP, hIJ⟩ := Ideal.exists_le_maximal _ hIJ
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
have rw : [IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J, IsCoprime I J].TFAE
Tactic: rw [← isCoprime_iff_codisjoint, ← isCoprime_iff_add, ← isCoprime_iff_exists,
      ← isCoprime_iff_sup_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
⊢ IsCoprime (R := Ideal R) (span {x}) (span {y}) ↔ IsCoprime x y
have simp_rw : (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
Tactic: simp_rw [isCoprime_iff_codisjoint, codisjoint_iff, eq_top_iff_one, mem_span_singleton_sup,
    mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
⊢ (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
have mp : (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) → IsCoprime x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
x y : R
mp : (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) → IsCoprime x y
⊢ (∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y
have mpr : IsCoprime x y → ∃ (a : R) (b : R), y ∣ b ∧ a * x + b = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
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)
⊢ IsCoprime I (⨅ j ∈ s, J j)
have simp : ∀ (hf : ∀ j ∈ s, I + J j = ⊤), I + ⨅ j ∈ s, J j = ⊤
Tactic: simp only [isCoprime_iff_add, one_eq_top] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑(insert a s) : Set ι).Pairwise (IsCoprime on J)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ insert a s, J i) (⨅ i ∈ insert a s, J i)
have insert : ∀ (ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
  (hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a),
  J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
Tactic: simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
Cleared hypotheses: ih, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
have hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
Tactic: obtain ⟨hp1, hp2⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp : (↑s : Set ι).Pairwise (IsCoprime on J) ∧ ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
have hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
Tactic: obtain ⟨hp1, hp2⟩ := hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
J : ι → Ideal R
a : ι
s : Finset ι
hs : a ∉ s
ih : Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
hp1 : (↑s : Set ι).Pairwise (IsCoprime on J)
hp2 : ∀ b ∈ s, ¬a = b → (IsCoprime on J) a b ∧ (IsCoprime on J) b a
⊢ J a * ⨅ i ∈ s, J i = J a ⊓ ⨅ x ∈ s, J x
have insert : J a ⊓ ⨅ j ∈ s, J j = J a ⊓ ⨅ x ∈ s, J x
Tactic: rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
have empty : ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
  Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]
Cleared hypotheses: s, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
empty :
  ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
have insert : ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
  (ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
  (hp : (↑(insert a s) : Set ι).Pairwise (IsCoprime on J)),
  Eq.{u + 1} (α := Ideal R) (∏ i ∈ insert a s, J i) (⨅ i ∈ insert a s, J i)
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]
Cleared hypotheses: s, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
have empty : ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
  Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]
Cleared hypotheses: s, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
s : Finset ι
J : ι → Ideal R
hp : (↑s : Set ι).Pairwise (IsCoprime on J)
empty :
  ∀ (hp : (↑∅ : Set ι).Pairwise (IsCoprime on J)),
    Eq.{u + 1} (α := Ideal R) (∏ i ∈ ∅, J i) (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Finset ι) ∅ i), J i)
⊢ Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i)
have insert : ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
  (ih : ∀ (hp : (↑s : Set ι).Pairwise (IsCoprime on J)), Eq.{u + 1} (α := Ideal R) (∏ i ∈ s, J i) (⨅ i ∈ s, J i))
  (hp : (↑(insert a s) : Set ι).Pairwise (IsCoprime on J)),
  Eq.{u + 1} (α := Ideal R) (∏ i ∈ insert a s, J i) (⨅ i ∈ insert a s, J i)
Tactic: classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s hs ih =>
    simp_all only [Finset.iInf_insert, Finset.coe_insert, Set.pairwise_insert, SetLike.mem_coe,
      ne_eq, not_false_eq_true, Finset.prod_insert, forall_const]
    obtain ⟨hp1, hp2⟩ := hp
    rw [Ideal.mul_eq_inf_of_isCoprime (isCoprime_biInf (by grind))]
Cleared hypotheses: s, hp
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I.radical = I ↔ I.IsRadical
have rw : I.radical ≤ I ∧ I ≤ I.radical ↔ I.IsRadical
Tactic: rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
rw : I.radical ≤ I ∧ I ≤ I.radical ↔ I.IsRadical
⊢ I.radical = I ↔ I.IsRadical
have rw₁ : I.radical ≤ I ↔ I.IsRadical
Tactic: rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
rw : I.radical ≤ I ∧ I ≤ I.radical ↔ I.IsRadical
rw₁ : I.radical ≤ I ↔ I.IsRadical
⊢ I.radical = I ↔ I.IsRadical
have rw₂ : I.radical ≤ I ↔ I.radical ≤ I
Tactic: rw [le_antisymm_iff, and_iff_left le_radical, IsRadical]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
y : R
hI : I.IsRadical
⊢ Disjoint (↑(Submonoid.powers y) : Set R) (↑I : Set R) ↔ y ∉ I
have refine : ∀ (h : y ∉ I), (↑(Submonoid.powers y) : Set R) ⊓ (↑I : Set R) ≤ ⊥
Tactic: refine ⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _),
      fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).IsRadical
have rw : I.radical ⊓ J.radical ≤ I ⊓ J
Tactic: rw [IsRadical, radical_inf]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
ι : Type u_2
s : Finset ι
f : ι → Ideal R
i : ι
hi : i ∈ s
hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical
⊢ (s.inf f).radical = (f i).radical
have rw : s.inf' sorry ((⇑radicalInfTopHom : (a : Ideal R) → Ideal R) ∘ f) = (f i).radical
Tactic: rw [← radicalInfTopHom_apply, map_finset_inf, ← Finset.inf'_eq_inf ⟨_, hi⟩]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I * J).radical = I.radical ⊓ J.radical
have refine : (I * J).radical ≤ I.radical ⊓ J.radical
Tactic: refine le_antisymm ?_ fun r ⟨⟨m, hrm⟩, ⟨n, hrn⟩⟩ =>
    ⟨m + n, (pow_add r m n).symm ▸ mul_mem_mul hrm hrn⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
I J : Ideal R
⊢ (I * J).radical ≤ I.radical ⊓ J.radical
have this : (I * J).radical ≤ (I ⊓ J).radical
Tactic: have := radical_mono <| mul_le_inf (I := I) (J := J)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Operations (goal)
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
r : R
hr : Membership.mem (γ := Submodule R R) (sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}) r
hri : r ∉ I.radical
m : Ideal R
hIm : I ≤ m
hm : Maximal (fun (x : Ideal R) ↦ Membership.mem (γ := Set (Ideal R)) {K : Ideal R | r ∉ K.radical} x) m
hrm : r ∉ m.radical
x : R
hxm : x ∉ m
hrmx : r ∉ (m ⊔ span {x}).radical
⊢ x ∈ m
have rw : x ∈ m ⊔ span {x}
Tactic: rw [hm.eq_of_le hrmx le_sup_left]