R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∃ r x, r ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
⊢ ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
intro j hjs hji
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
hf : f i ⊔ f j = ⊤
⊢ ∃ r x, r ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∃ r x, r ∈ f j
specialize hf i his j hjs hji.symm
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
hf : ∃ y, y ∈ f i ∧ ∃ z, z ∈ f j ∧ y + z = 1
⊢ ∃ r x, r ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
hf : f i ⊔ f j = ⊤
⊢ ∃ r x, r ∈ f j
rw [eq_top_iff_one, Submodule.mem_sup] at hf
case intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ ∃ r x, r ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s
j : ι
hjs : j ∈ s
hji : j ≠ i
hf : ∃ y, y ∈ f i ∧ ∃ z, z ∈ f j ∧ y + z = 1
⊢ ∃ r x, r ∈ f j
rcases hf with ⟨r, hri, s, hsj, hrs⟩
case intro.intro.intro.intro.refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ 1 - r - 1 ∈ f i

case intro.intro.intro.intro.refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ 1 - r ∈ f j
case intro.intro.intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ ∃ r x, r ∈ f j
refine' ⟨1 - r, _, _⟩
case intro.intro.intro.intro.refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ -r ∈ f i
case intro.intro.intro.intro.refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ 1 - r - 1 ∈ f i
rw [sub_right_comm, sub_self, zero_sub]
no goals
case intro.intro.intro.intro.refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ -r ∈ f i
exact (f i).neg_mem hri
case intro.intro.intro.intro.refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ s ∈ f j
case intro.intro.intro.intro.refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ 1 - r ∈ f j
rw [← hrs, add_sub_cancel']
no goals
case intro.intro.intro.intro.refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s✝ : Finset ι
f : ι → Ideal R
i : ι
his : i ∈ s✝
j : ι
hjs : j ∈ s✝
hji : j ≠ i
r : R
hri : r ∈ f i
s : R
hsj : s ∈ f j
hrs : r + s = 1
⊢ s ∈ f j
exact hsj
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
this : ∃ g, (∀ (j : ι), g j - 1 ∈ f i) ∧ ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
rcases this with ⟨g, hgi, hgj⟩
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, g x - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → ∏ x in Finset.erase s i, g x ∈ f j
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
use ∏ x in s.erase i, g x
case intro.intro.left
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, g x - 1 ∈ f i

case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∀ (j : ι), j ∈ s → j ≠ i → ∏ x in Finset.erase s i, g x ∈ f j
case intro.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, g x - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → ∏ x in Finset.erase s i, g x ∈ f j
constructor
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
⊢ ∃ g, (∀ (j : ι), g j - 1 ∈ f i) ∧ ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
⊢ ∃ g, (∀ (j : ι), g j - 1 ∈ f i) ∧ ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
choose g hg1 hg2 using this
case refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j - 1 ∈ f i

case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ j ∈ s → j ≠ i → (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j ∈ f j
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
⊢ ∃ g, (∀ (j : ι), g j - 1 ∈ f i) ∧ ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
refine' ⟨fun j => if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, fun j => _, fun j => _⟩
case refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ (if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) - 1 ∈ f i
case refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j - 1 ∈ f i
dsimp only
case refine'_1.inl
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : j ∈ s ∧ j ≠ i
⊢ g j (_ : j ∈ s) (_ : j ≠ i) - 1 ∈ f i

case refine'_1.inr
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : ¬(j ∈ s ∧ j ≠ i)
⊢ 1 - 1 ∈ f i
case refine'_1
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ (if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) - 1 ∈ f i
split_ifs with h
case refine'_1.inr
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : ¬(j ∈ s ∧ j ≠ i)
⊢ 0 ∈ f i
case refine'_1.inr
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : ¬(j ∈ s ∧ j ≠ i)
⊢ 1 - 1 ∈ f i
rw [sub_self]
no goals
case refine'_1.inr
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : ¬(j ∈ s ∧ j ≠ i)
⊢ 0 ∈ f i
exact (f i).zero_mem
no goals
case refine'_1.inl
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
h : j ∈ s ∧ j ≠ i
⊢ g j (_ : j ∈ s) (_ : j ≠ i) - 1 ∈ f i
apply hg1
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j ∈ f j
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
⊢ j ∈ s → j ≠ i → (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j ∈ f j
intro hjs hji
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ (if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) ∈ f j
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ (fun j => if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) j ∈ f j
dsimp only
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ g j (_ : j ∈ s) (_ : j ≠ i) ∈ f j

case refine'_2.hc
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ j ∈ s ∧ j ≠ i
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ (if H : j ∈ s ∧ j ≠ i then g j (_ : j ∈ s) (_ : j ≠ i) else 1) ∈ f j
rw [dif_pos]
no goals
case refine'_2.hc
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ j ∈ s ∧ j ≠ i
exact ⟨hjs, hji⟩
no goals
case refine'_2
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
g : (j : ι) → j ∈ s → j ≠ i → R
hg1 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 - 1 ∈ f i
hg2 : ∀ (j : ι) (a : j ∈ s) (a_1 : j ≠ i), g j a a_1 ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ g j (_ : j ∈ s) (_ : j ≠ i) ∈ f j
apply hg2
case intro.intro.left
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f i)) (g x) = 1
case intro.intro.left
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, g x - 1 ∈ f i
rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, map_one, map_prod]
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∀ (x : ι), x ∈ Finset.erase s i → ↑(Quotient.mk (f i)) (g x) = 1
case intro.intro.left
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f i)) (g x) = 1
apply Finset.prod_eq_one
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
x✝ : ι
a✝ : x✝ ∈ Finset.erase s i
⊢ ↑(Quotient.mk (f i)) (g x✝) = 1
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∀ (x : ι), x ∈ Finset.erase s i → ↑(Quotient.mk (f i)) (g x) = 1
intros
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
x✝ : ι
a✝ : x✝ ∈ Finset.erase s i
⊢ g x✝ - 1 ∈ f i
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
x✝ : ι
a✝ : x✝ ∈ Finset.erase s i
⊢ ↑(Quotient.mk (f i)) (g x✝) = 1
rw [← RingHom.map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
no goals
case intro.intro.left.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
x✝ : ι
a✝ : x✝ ∈ Finset.erase s i
⊢ g x✝ - 1 ∈ f i
apply hgi
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∏ x in Finset.erase s i, g x ∈ f j
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
⊢ ∀ (j : ι), j ∈ s → j ≠ i → ∏ x in Finset.erase s i, g x ∈ f j
intro j hjs hji
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f j)) (g x) = 0
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∏ x in Finset.erase s i, g x ∈ f j
rw [← Quotient.eq_zero_iff_mem, map_prod]
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f j)) (g x) = 0
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f j)) (g x) = 0
letI : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ ↑(Quotient.mk (f j)) (g j) = 0
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ ∏ x in Finset.erase s i, ↑(Quotient.mk (f j)) (g x) = 0
refine' Finset.prod_eq_zero (Finset.mem_erase_of_ne_of_mem hji hjs) _
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ g j ∈ f j
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ ↑(Quotient.mk (f j)) (g j) = 0
rw [Quotient.eq_zero_iff_mem]
no goals
case intro.intro.right
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
s : Finset ι
f : ι → Ideal R
hf : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ⊔ f j = ⊤
i : ι
his : i ∈ s
this✝ : ∀ (j : ι), j ∈ s → j ≠ i → ∃ r x, r ∈ f j
g : ι → R
hgi : ∀ (j : ι), g j - 1 ∈ f i
hgj : ∀ (j : ι), j ∈ s → j ≠ i → g j ∈ f j
j : ι
hjs : j ∈ s
hji : j ≠ i
this : CommMonoidWithZero (R ⧸ f j) := CommSemiring.toCommMonoidWithZero
⊢ g j ∈ f j
exact hgj j hjs hji