case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
cases nonempty_fintype ι
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
this : ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
have : ∃ φ : ι → R, (∀ i, φ i - 1 ∈ f i) ∧ ∀ i j, i ≠ j → φ i ∈ f j := by
  have := exists_sub_one_mem_and_mem (Finset.univ : Finset ι) fun i _ j _ hij => hf i j hij
  choose φ hφ using this
  exists fun i => φ i (Finset.mem_univ i)
  exact ⟨fun i => (hφ i _).1, fun i j hij => (hφ i _).2 j (Finset.mem_univ j) hij.symm⟩
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
this : ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
rcases this with ⟨φ, hφ1, hφ2⟩
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∀ (i : ι), ∑ i : ι, g i * φ i - g i ∈ f i
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∃ r, ∀ (i : ι), r - g i ∈ f i
use ∑ i, g i * φ i
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∑ i : ι, g i * φ i - g i ∈ f i
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
⊢ ∀ (i : ι), ∑ i : ι, g i * φ i - g i ∈ f i
intro i
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∑ x : ι, ↑(Quotient.mk (f i)) (g x * φ x) = ↑(Quotient.mk (f i)) (g i)
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∑ i : ι, g i * φ i - g i ∈ f i
rw [← Quotient.mk_eq_mk_iff_sub_mem, map_sum]
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∀ (b : ι), b ∈ Finset.univ → b ≠ i → ↑(Quotient.mk (f i)) (g b * φ b) = 0

case intro.intro.intro.refine'_2
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ¬i ∈ Finset.univ → ↑(Quotient.mk (f i)) (g i * φ i) = 0

case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
case intro.intro.intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∑ x : ι, ↑(Quotient.mk (f i)) (g x * φ x) = ↑(Quotient.mk (f i)) (g i)
refine' Eq.trans (Finset.sum_eq_single i _ _) _
case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hφ1 : φ i - 1 ∈ f i
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
specialize hφ1 i
case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hφ1 : ↑(Quotient.mk (f i)) (φ i) = 1
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hφ1 : φ i - 1 ∈ f i
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
rw [← Quotient.mk_eq_mk_iff_sub_mem, RingHom.map_one] at hφ1
no goals
case intro.intro.intro.refine'_3
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hφ1 : ↑(Quotient.mk (f i)) (φ i) = 1
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = ↑(Quotient.mk (f i)) (g i)
rw [RingHom.map_mul, hφ1, mul_one]
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
this : ∀ (i : ι), i ∈ Finset.univ → ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → r ∈ f j
⊢ ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
⊢ ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
have := exists_sub_one_mem_and_mem (Finset.univ : Finset ι) fun i _ j _ hij => hf i j hij
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : (i : ι) → i ∈ Finset.univ → R
hφ : ∀ (i : ι) (his : i ∈ Finset.univ), φ i his - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → φ i his ∈ f j
⊢ ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
this : ∀ (i : ι), i ∈ Finset.univ → ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → r ∈ f j
⊢ ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
choose φ hφ using this
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : (i : ι) → i ∈ Finset.univ → R
hφ : ∀ (i : ι) (his : i ∈ Finset.univ), φ i his - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → φ i his ∈ f j
⊢ (∀ (i : ι), (fun i => φ i (_ : i ∈ Finset.univ)) i - 1 ∈ f i) ∧
    ∀ (i j : ι), i ≠ j → (fun i => φ i (_ : i ∈ Finset.univ)) i ∈ f j
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : (i : ι) → i ∈ Finset.univ → R
hφ : ∀ (i : ι) (his : i ∈ Finset.univ), φ i his - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → φ i his ∈ f j
⊢ ∃ φ, (∀ (i : ι), φ i - 1 ∈ f i) ∧ ∀ (i j : ι), i ≠ j → φ i ∈ f j
exists fun i => φ i (Finset.mem_univ i)
no goals
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : (i : ι) → i ∈ Finset.univ → R
hφ : ∀ (i : ι) (his : i ∈ Finset.univ), φ i his - 1 ∈ f i ∧ ∀ (j : ι), j ∈ Finset.univ → j ≠ i → φ i his ∈ f j
⊢ (∀ (i : ι), (fun i => φ i (_ : i ∈ Finset.univ)) i - 1 ∈ f i) ∧
    ∀ (i j : ι), i ≠ j → (fun i => φ i (_ : i ∈ Finset.univ)) i ∈ f j
exact ⟨fun i => (hφ i _).1, fun i j hij => (hφ i _).2 j (Finset.mem_univ j) hij.symm⟩
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i j : ι
a✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ ↑(Quotient.mk (f i)) (g j * φ j) = 0
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ∀ (b : ι), b ∈ Finset.univ → b ≠ i → ↑(Quotient.mk (f i)) (g b * φ b) = 0
intro j _ hji
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i j : ι
a✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ g j * φ j ∈ f i
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i j : ι
a✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ ↑(Quotient.mk (f i)) (g j * φ j) = 0
rw [Quotient.eq_zero_iff_mem]
no goals
case intro.intro.intro.refine'_1
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i j : ι
a✝ : j ∈ Finset.univ
hji : j ≠ i
⊢ g j * φ j ∈ f i
exact (f i).mul_mem_left _ (hφ2 j i hji)
case intro.intro.intro.refine'_2
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hi : ¬i ∈ Finset.univ
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = 0
case intro.intro.intro.refine'_2
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
⊢ ¬i ∈ Finset.univ → ↑(Quotient.mk (f i)) (g i * φ i) = 0
intro hi
no goals
case intro.intro.intro.refine'_2
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι : Type v
inst✝ : Finite ι
f : ι → Ideal R
hf : ∀ (i j : ι), i ≠ j → f i ⊔ f j = ⊤
g : ι → R
val✝ : Fintype ι
φ : ι → R
hφ1 : ∀ (i : ι), φ i - 1 ∈ f i
hφ2 : ∀ (i j : ι), i ≠ j → φ i ∈ f j
i : ι
hi : ¬i ∈ Finset.univ
⊢ ↑(Quotient.mk (f i)) (g i * φ i) = 0
exact (hi <| Finset.mem_univ i).elim