-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_biInf {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j)

Proof state:
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)

Tactic:
simp_rw [isCoprime_iff_add] at *

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1

Proof state:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ j ∈ insert i s, J j = 1

Tactic:
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]

Result:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ x ∈ s, J x) ⊓ J i

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K * (I + J i) = (1 + K) * I + K * J i

Tactic:
ring

Result:
no goals

Proof state:
case empty
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
hf : ∀ j ∈ ∅, I + J j = 1
⊢ I + ⨅ j ∈ ∅, J j = 1

Tactic:
simp

Result:
no goals

Proof state:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ j ∈ s, J j = 1
hf : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ x ∈ s, J x) ⊓ J i

Tactic:
set K := ⨅ j ∈ s, J j

Result:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1

Tactic:
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K            := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf

Result:
no goals

Proof state:
case insert
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i

Tactic:
calc
  1 = I + K            := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
  _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
  _ = (1+K)*I + K*J i  := by ring
  _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf

Result:
no goals

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ j ∈ s, J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K = I + K * (I + J i)

Tactic:
rw [hf i (Finset.mem_insert_self i s), mul_one]

Result:
no goals

Proof state:
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)

Tactic:
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K            := (hs fun j hj ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf

Result:
no goals