Theorem: Ideal.coprime_iInf_of_coprime (LCTutorial/Solutions/Topics/ChineseRemainder.lean)

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
Tactic:
revert hf
State after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
⊢ (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
⊢ (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
Tactic:
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    intro h
    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 ↦ h j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [h 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
State after:
no goals

State before:
case empty
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
⊢ (∀ j ∈ ∅, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ ∅), J j = 1
Tactic:
simp
State after:
no goals

State before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
⊢ (∀ j ∈ insert i s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
Tactic:
intro h
State after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1

State before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
Tactic:
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
State after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ (x : ι) (_ : x ∈ s), J x) ⊓ J i

State before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ (x : ι) (_ : x ∈ s), J x) ⊓ J i
Tactic:
set K := ⨅ j ∈ s, J j
State after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i

State before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : 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 ↦ h j (Finset.mem_insert_of_mem hj)).symm
  _ = I + K*(I + J i)  := by rw [h 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
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K = I + K * (I + J i)
Tactic:
rw [h i (Finset.mem_insert_self i s), mul_one]
State after:
no goals

State before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : 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
State after:
no goals