[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
src✝ : AddCon R := QuotientAddGroup.con (Submodule.toAddSubgroup I)
a₁ b₁ a₂ b₂ : R
h₁ : Setoid.r a₁ b₁
h₂ : Setoid.r a₂ b₂
⊢ Setoid.r (a₁ * a₂) (b₁ * b₂)
[PROOFSTEP]
rw [Submodule.quotientRel_r_def] at h₁ h₂ ⊢
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
src✝ : AddCon R := QuotientAddGroup.con (Submodule.toAddSubgroup I)
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I
[PROOFSTEP]
have F := I.add_mem (I.mul_mem_left a₂ h₁) (I.mul_mem_right b₁ h₂)
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
src✝ : AddCon R := QuotientAddGroup.con (Submodule.toAddSubgroup I)
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
F : a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I
[PROOFSTEP]
have : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ := by
  rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
src✝ : AddCon R := QuotientAddGroup.con (Submodule.toAddSubgroup I)
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
F : a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁
[PROOFSTEP]
rw [mul_sub, sub_mul, sub_add_sub_cancel, mul_comm, mul_comm b₁]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
src✝ : AddCon R := QuotientAddGroup.con (Submodule.toAddSubgroup I)
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
F : a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁ ∈ I
this : a₁ * a₂ - b₁ * b₂ = a₂ * (a₁ - b₁) + (a₂ - b₂) * b₁
⊢ a₁ * a₂ - b₁ * b₂ ∈ I
[PROOFSTEP]
rwa [← this] at F
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S : Type v
x✝ y✝ x y : R
⊢ ↑(mk I) x = ↑(mk I) y ↔ x - y ∈ I
[PROOFSTEP]
rw [← eq_zero_iff_mem, map_sub, sub_eq_zero]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
⊢ Subsingleton (R ⧸ I) ↔ I = ⊤
[PROOFSTEP]
rw [eq_top_iff_one, ← subsingleton_iff_zero_eq_one, eq_comm, ← (mk I).map_one, Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S : Type v
x y : R
⊢ ∀ (a : R ⧸ ⊤), a = default
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S : Type v
x✝ y : R
a✝ : R ⧸ ⊤
x : R
⊢ Quot.mk Setoid.r x = default
[PROOFSTEP]
exact Quotient.eq_zero_iff_mem.mpr Submodule.mem_top
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
s : Set R
⊢ ↑(mk I) ⁻¹' (↑(mk I) '' s) = ⋃ (x : { x // x ∈ I }), (fun y => ↑x + y) '' s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ x ∈ ↑(mk I) ⁻¹' (↑(mk I) '' s) ↔ x ∈ ⋃ (x : { x // x ∈ I }), (fun y => ↑x + y) '' s
[PROOFSTEP]
simp only [mem_preimage, mem_image, mem_iUnion, Ideal.Quotient.eq]
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
s : Set R
x : R
⊢ (∃ x_1, x_1 ∈ s ∧ x_1 - x ∈ I) ↔ ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
[PROOFSTEP]
exact
  ⟨fun ⟨a, a_in, h⟩ => ⟨⟨_, I.neg_mem h⟩, a, a_in, by simp⟩, fun ⟨⟨i, hi⟩, a, ha, Eq⟩ =>
    ⟨a, ha, by rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]; exact I.neg_mem hi⟩⟩
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ x_1, x_1 ∈ s ∧ x_1 - x ∈ I
a : R
a_in : a ∈ s
h : a - x ∈ I
⊢ ↑{ val := -(a - x), property := (_ : -(a - x) ∈ I) } + a = x
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑{ val := i, property := hi } + a = x
⊢ a - x ∈ I
[PROOFSTEP]
rw [← Eq, sub_add_eq_sub_sub_swap, sub_self, zero_sub]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x✝¹ y : R
I : Ideal R
s : Set R
x : R
x✝ : ∃ i x_1, x_1 ∈ s ∧ ↑i + x_1 = x
i : R
hi : i ∈ I
a : R
ha : a ∈ s
Eq : ↑{ val := i, property := hi } + a = x
⊢ -↑{ val := i, property := hi } ∈ I
[PROOFSTEP]
exact I.neg_mem hi
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
⊢ IsDomain (R ⧸ I) ↔ IsPrime I
[PROOFSTEP]
refine' ⟨fun H => ⟨zero_ne_one_iff.1 _, fun {x y} h => _⟩, fun h => inferInstance⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
⊢ 0 ≠ 1
[PROOFSTEP]
haveI : Nontrivial (R ⧸ I) := ⟨H.2.1⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
H : IsDomain (R ⧸ I)
this : Nontrivial (R ⧸ I)
⊢ 0 ≠ 1
[PROOFSTEP]
exact zero_ne_one
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : x * y ∈ I
⊢ x ∈ I ∨ y ∈ I
[PROOFSTEP]
simp only [← eq_zero_iff_mem, (mk I).map_mul] at h ⊢
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
[PROOFSTEP]
haveI := @IsDomain.to_noZeroDivisors (R ⧸ I) _ H
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
H : IsDomain (R ⧸ I)
x y : R
h : ↑(mk I) x * ↑(mk I) y = 0
this : NoZeroDivisors (R ⧸ I)
⊢ ↑(mk I) x = 0 ∨ ↑(mk I) y = 0
[PROOFSTEP]
exact eq_zero_or_eq_zero_of_mul_eq_zero h
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
⊢ ∀ {a : R ⧸ I}, a ≠ 0 → ∃ b, a * b = 1
[PROOFSTEP]
rintro ⟨a⟩ h
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
[PROOFSTEP]
rcases hI.exists_inv (mt eq_zero_iff_mem.2 h) with ⟨b, c, hc, abc⟩
[GOAL]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : b * a + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
[PROOFSTEP]
rw [mul_comm] at abc
[GOAL]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ ∃ b, Quot.mk Setoid.r a * b = 1
[PROOFSTEP]
refine' ⟨mk _ b, Quot.sound _⟩
[GOAL]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ Setoid.r ((fun x x_1 => x * x_1) a b) 1
[PROOFSTEP]
simp only [Submodule.quotientRel_r_def]
[GOAL]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : a * b + c = 1
⊢ a * b - 1 ∈ I
[PROOFSTEP]
rw [← eq_sub_iff_add_eq'] at abc
[GOAL]
case mk.intro.intro.intro
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝¹ b✝ : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a✝ : R ⧸ I
a : R
h : Quot.mk Setoid.r a ≠ 0
b c : R
hc : c ∈ I
abc : c = 1 - a * b
⊢ a * b - 1 ∈ I
[PROOFSTEP]
rwa [abc, ← neg_mem_iff (G := R) (H := I), neg_sub] at hc
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a : R ⧸ I
ha : a ≠ 0
⊢ (a * if ha : a = 0 then 0 else choose (_ : ∃ b, a * b = 1)) = 1
[PROOFSTEP]
rw [dif_neg ha]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a✝ b : R
S : Type v
x y : R
I : Ideal R
hI : IsMaximal I
a : R ⧸ I
ha : a ≠ 0
⊢ a * choose (_ : ∃ b, a * b = 1) = 1
[PROOFSTEP]
exact Classical.choose_spec (exists_inv ha)
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ IsMaximal I
[PROOFSTEP]
apply Ideal.isMaximal_iff.2
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ¬1 ∈ I
[PROOFSTEP]
intro h
[GOAL]
case left
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
⊢ False
[PROOFSTEP]
rcases hqf.exists_pair_ne with ⟨⟨x⟩, ⟨y⟩, hxy⟩
[GOAL]
case left.intro.mk.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
h : 1 ∈ I
w✝¹ : R ⧸ I
x : R
w✝ : R ⧸ I
y : R
hxy : Quot.mk Setoid.r x ≠ Quot.mk Setoid.r y
⊢ False
[PROOFSTEP]
exact hxy (Ideal.Quotient.eq.2 (mul_one (x - y) ▸ I.mul_mem_left _ h))
[GOAL]
case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
hqf : IsField (R ⧸ I)
⊢ ∀ (J : Ideal R) (x : R), I ≤ J → ¬x ∈ I → x ∈ J → 1 ∈ J
[PROOFSTEP]
intro J x hIJ hxnI hxJ
[GOAL]
case right
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
⊢ 1 ∈ J
[PROOFSTEP]
rcases hqf.mul_inv_cancel (mt Ideal.Quotient.eq_zero_iff_mem.1 hxnI) with ⟨⟨y⟩, hy⟩
[GOAL]
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ 1 ∈ J
[PROOFSTEP]
rw [← zero_add (1 : R), ← sub_self (x * y), sub_add]
[GOAL]
case right.intro.mk
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y✝ : R
I : Ideal R
hqf : IsField (R ⧸ I)
J : Ideal R
x : R
hIJ : I ≤ J
hxnI : ¬x ∈ I
hxJ : x ∈ J
w✝ : R ⧸ I
y : R
hy : ↑(mk I) x * Quot.mk Setoid.r y = 1
⊢ x * y - (x * y - 1) ∈ J
[PROOFSTEP]
refine' J.sub_mem (J.mul_mem_right _ hxJ) (hIJ (Ideal.Quotient.eq.1 hy))
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
⊢ Function.Surjective ↑(lift I f H)
[PROOFSTEP]
intro y
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x y✝ : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
y : S
⊢ ∃ a, ↑(lift I f H) a = y
[PROOFSTEP]
obtain ⟨x, rfl⟩ := hf y
[GOAL]
case intro
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ∃ a, ↑(lift I f H) a = ↑f x
[PROOFSTEP]
use Ideal.Quotient.mk I x
[GOAL]
case h
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
x✝ y : R
inst✝ : CommRing S
I : Ideal R
f : R →+* S
H : ∀ (a : R), a ∈ I → ↑f a = 0
hf : Function.Surjective ↑f
x : R
⊢ ↑(lift I f H) (↑(mk I) x) = ↑f x
[PROOFSTEP]
simp only [Ideal.Quotient.lift_mk]
[GOAL]
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S✝ : Type v
x y : R
inst✝ : CommRing S✝
S T : Ideal R
H : S ≤ T
⊢ RingHom.comp (factor S T H) (mk S) = mk T
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S✝ : Type v
x✝ y : R
inst✝ : CommRing S✝
S T : Ideal R
H : S ≤ T
x : R
⊢ ↑(RingHom.comp (factor S T H) (mk S)) x = ↑(mk T) x
[PROOFSTEP]
rw [RingHom.comp_apply, factor_mk]
[GOAL]
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
src✝ : (R ⧸ I) ≃ₗ[R] R ⧸ J := Submodule.quotEquivOfEq I J h
⊢ ∀ (x y : R ⧸ I),
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (x * y) =
      Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          x *
        Equiv.toFun
          { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
          y
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩
[GOAL]
case mk.mk
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
src✝ : (R ⧸ I) ≃ₗ[R] R ⧸ J := Submodule.quotEquivOfEq I J h
x✝ : R ⧸ I
x : R
y✝ : R ⧸ I
y : R
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (Quot.mk Setoid.r x * Quot.mk Setoid.r y) =
    Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (Quot.mk Setoid.r x) *
      Equiv.toFun
        { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (Quot.mk Setoid.r y)
[PROOFSTEP]
rfl
[GOAL]
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
⊢ RingEquiv.symm (quotEquivOfEq h) = quotEquivOfEq (_ : J = I)
[PROOFSTEP]
ext
[GOAL]
case h
R✝ : Type u
inst✝¹ : CommRing R✝
I✝ : Ideal R✝
a b : R✝
S : Type v
R : Type u_1
inst✝ : CommRing R
I J : Ideal R
h : I = J
x✝ : R ⧸ J
⊢ ↑(RingEquiv.symm (quotEquivOfEq h)) x✝ = ↑(quotEquivOfEq (_ : J = I)) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
c : R ⧸ I
m : (ι → R) ⧸ pi I ι
⊢ ∀ (a₁ : R) (a₂ : ι → R) (b₁ : R) (b₂ : ι → R),
    Setoid.r a₁ b₁ →
      Setoid.r a₂ b₂ →
        (fun r m => Submodule.Quotient.mk (r • m)) a₁ a₂ = (fun r m => Submodule.Quotient.mk (r • m)) b₁ b₂
[PROOFSTEP]
intro c₁ m₁ c₂ m₂ hc hm
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
c : R ⧸ I
m : (ι → R) ⧸ pi I ι
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : Setoid.r c₁ c₂
hm : Setoid.r m₁ m₂
⊢ (fun r m => Submodule.Quotient.mk (r • m)) c₁ m₁ = (fun r m => Submodule.Quotient.mk (r • m)) c₂ m₂
[PROOFSTEP]
apply Ideal.Quotient.eq.2
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
c : R ⧸ I
m : (ι → R) ⧸ pi I ι
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : Setoid.r c₁ c₂
hm : Setoid.r m₁ m₂
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi I ι
[PROOFSTEP]
rw [Submodule.quotientRel_r_def] at hc hm
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
c : R ⧸ I
m : (ι → R) ⧸ pi I ι
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : c₁ - c₂ ∈ I
hm : m₁ - m₂ ∈ pi I ι
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi I ι
[PROOFSTEP]
intro i
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
c : R ⧸ I
m : (ι → R) ⧸ pi I ι
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : c₁ - c₂ ∈ I
hm : m₁ - m₂ ∈ pi I ι
i : ι
⊢ (c₁ • m₁ - c₂ • m₂) i ∈ I
[PROOFSTEP]
exact I.mul_sub_mul_mem hc (hm i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (b : (ι → R) ⧸ pi I ι), 1 • b = b
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
b✝ : (ι → R) ⧸ pi I ι
a : ι → R
⊢ 1 • Quot.mk Setoid.r a = Quot.mk Setoid.r a
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
b✝ : (ι → R) ⧸ pi I ι
a : ι → R
⊢ ↑(Quotient.mk (pi I ι)) (1 • a) = ↑(Quotient.mk (pi I ι)) a
[PROOFSTEP]
congr with i
[GOAL]
case mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
b✝ : (ι → R) ⧸ pi I ι
a : ι → R
i : ι
⊢ (1 • a) i = a i
[PROOFSTEP]
exact one_mul (a i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (x y : R ⧸ I) (b : (ι → R) ⧸ pi I ι), (x * y) • b = x • y • b
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩
[GOAL]
case mk.mk.mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝¹ : R
S ι : Type v
x✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ (Quot.mk Setoid.r a * Quot.mk Setoid.r b) • Quot.mk Setoid.r c =
    Quot.mk Setoid.r a • Quot.mk Setoid.r b • Quot.mk Setoid.r c
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.mk.mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝¹ : R
S ι : Type v
x✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ ↑(Quotient.mk (pi I ι)) ((fun x x_1 => x * x_1) a b • c) = ↑(Quotient.mk (pi I ι)) (a • b • c)
[PROOFSTEP]
congr 1
[GOAL]
case mk.mk.mk.convert_3.h.e_6.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝¹ : R
S ι : Type v
x✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ (fun x x_1 => x * x_1) a b • c = a • b • c
[PROOFSTEP]
funext i
[GOAL]
case mk.mk.mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝¹ : R
S ι : Type v
x✝ : R ⧸ I
a : R
y✝ : R ⧸ I
b : R
b✝ : (ι → R) ⧸ pi I ι
c : ι → R
i : ι
⊢ ((fun x x_1 => x * x_1) a b • c) i = (a • b • c) i
[PROOFSTEP]
exact mul_assoc a b (c i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (a : R ⧸ I), a • 0 = 0
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b : R
S ι : Type v
a✝ : R ⧸ I
a : R
⊢ Quot.mk Setoid.r a • 0 = 0
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b : R
S ι : Type v
a✝ : R ⧸ I
a : R
⊢ ↑(Quotient.mk (pi I ι)) (a • 0) = ↑(Quotient.mk (pi I ι)) 0
[PROOFSTEP]
congr with _
[GOAL]
case mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b : R
S ι : Type v
a✝ : R ⧸ I
a : R
x✝ : ι
⊢ (a • 0) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
exact mul_zero a
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (a : R ⧸ I) (x y : (ι → R) ⧸ pi I ι), a • (x + y) = a • x + a • y
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩
[GOAL]
case mk.mk.mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b✝ : R
S ι : Type v
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi I ι
b : ι → R
y✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ Quot.mk Setoid.r a • (Quot.mk Setoid.r b + Quot.mk Setoid.r c) =
    Quot.mk Setoid.r a • Quot.mk Setoid.r b + Quot.mk Setoid.r a • Quot.mk Setoid.r c
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.mk.mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b✝ : R
S ι : Type v
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi I ι
b : ι → R
y✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ ↑(Quotient.mk (pi I ι)) (a • (fun x x_1 => x + x_1) b c) =
    ↑(Quotient.mk (pi I ι)) ((fun x x_1 => x + x_1) (a • b) (a • c))
[PROOFSTEP]
congr with i
[GOAL]
case mk.mk.mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝¹ b✝ : R
S ι : Type v
a✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ pi I ι
b : ι → R
y✝ : (ι → R) ⧸ pi I ι
c : ι → R
i : ι
⊢ (a • (fun x x_1 => x + x_1) b c) i = (fun x x_1 => x + x_1) (a • b) (a • c) i
[PROOFSTEP]
exact mul_add a (b i) (c i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (r s : R ⧸ I) (x : (ι → R) ⧸ pi I ι), (r + s) • x = r • x + s • x
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩
[GOAL]
case mk.mk.mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝ : R
S ι : Type v
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ (Quot.mk Setoid.r a + Quot.mk Setoid.r b) • Quot.mk Setoid.r c =
    Quot.mk Setoid.r a • Quot.mk Setoid.r c + Quot.mk Setoid.r b • Quot.mk Setoid.r c
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.mk.mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝ : R
S ι : Type v
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi I ι
c : ι → R
⊢ ↑(Quotient.mk (pi I ι)) ((fun x x_1 => x + x_1) a b • c) =
    ↑(Quotient.mk (pi I ι)) ((fun x x_1 => x + x_1) (a • c) (b • c))
[PROOFSTEP]
congr with i
[GOAL]
case mk.mk.mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b✝ : R
S ι : Type v
r✝ : R ⧸ I
a : R
s✝ : R ⧸ I
b : R
x✝ : (ι → R) ⧸ pi I ι
c : ι → R
i : ι
⊢ ((fun x x_1 => x + x_1) a b • c) i = (fun x x_1 => x + x_1) (a • c) (b • c) i
[PROOFSTEP]
exact add_mul a b (c i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (x : (ι → R) ⧸ pi I ι), 0 • x = 0
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
x✝ : (ι → R) ⧸ pi I ι
a : ι → R
⊢ 0 • Quot.mk Setoid.r a = 0
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case mk.convert_3
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
x✝ : (ι → R) ⧸ pi I ι
a : ι → R
⊢ ↑(Quotient.mk (pi I ι)) (0 • a) = ↑(Quotient.mk (pi I ι)) 0
[PROOFSTEP]
congr with i
[GOAL]
case mk.convert_3.h.e_6.h.h
R : Type u
inst✝ : CommRing R
I : Ideal R
a✝ b : R
S ι : Type v
x✝ : (ι → R) ⧸ pi I ι
a : ι → R
i : ι
⊢ (0 • a) i = OfNat.ofNat 0 i
[PROOFSTEP]
exact zero_mul (a i)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (x y : (ι → R) ⧸ pi I ι),
    (fun x =>
          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
            (_ :
              ∀ (a b : ι → R),
                Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
        (x + y) =
      (fun x =>
            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
              (_ :
                ∀ (a b : ι → R),
                  Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
          x +
        (fun x =>
            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
              (_ :
                ∀ (a b : ι → R),
                  Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
          y
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
x✝ : (ι → R) ⧸ pi I ι
a✝¹ : ι → R
y✝ : (ι → R) ⧸ pi I ι
a✝ : ι → R
⊢ (fun x =>
        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
          (_ :
            ∀ (a b : ι → R),
              Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
      (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) =
    (fun x =>
          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
            (_ :
              ∀ (a b : ι → R),
                Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
        (Quot.mk Setoid.r a✝¹) +
      (fun x =>
          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
            (_ :
              ∀ (a b : ι → R),
                Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
        (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
    AddHom.toFun
        {
          toFun := fun x =>
            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
              (_ :
                ∀ (a b : ι → R),
                  Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ pi I ι),
                (fun x =>
                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                        (_ :
                          ∀ (a b : ι → R),
                            Setoid.r a b →
                              (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                    (x + y) =
                  (fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                      x +
                    (fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                      y) }
        (r • x) =
      ↑(RingHom.id (R ⧸ I)) r •
        AddHom.toFun
          {
            toFun := fun x =>
              Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                (_ :
                  ∀ (a b : ι → R),
                    Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
            map_add' :=
              (_ :
                ∀ (x y : (ι → R) ⧸ pi I ι),
                  (fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                      (x + y) =
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        x +
                      (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        y) }
          x
[PROOFSTEP]
rintro ⟨_⟩ ⟨_⟩
[GOAL]
case mk.mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
r✝ : R ⧸ I
a✝¹ : R
x✝ : (ι → R) ⧸ pi I ι
a✝ : ι → R
⊢ AddHom.toFun
      {
        toFun := fun x =>
          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
            (_ :
              ∀ (a b : ι → R),
                Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ pi I ι),
              (fun x =>
                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                      (_ :
                        ∀ (a b : ι → R),
                          Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                  (x + y) =
                (fun x =>
                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                        (_ :
                          ∀ (a b : ι → R),
                            Setoid.r a b →
                              (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                    x +
                  (fun x =>
                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                        (_ :
                          ∀ (a b : ι → R),
                            Setoid.r a b →
                              (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                    y) }
      (Quot.mk Setoid.r a✝¹ • Quot.mk Setoid.r a✝) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a✝¹) •
      AddHom.toFun
        {
          toFun := fun x =>
            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
              (_ :
                ∀ (a b : ι → R),
                  Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ pi I ι),
                (fun x =>
                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                        (_ :
                          ∀ (a b : ι → R),
                            Setoid.r a b →
                              (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                    (x + y) =
                  (fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                      x +
                    (fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                      y) }
        (Quot.mk Setoid.r a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ Function.LeftInverse (fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i))
    {
          toAddHom :=
            {
              toFun := fun x =>
                Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                  (_ :
                    ∀ (a b : ι → R),
                      Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ pi I ι),
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        (x + y) =
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          x +
                        (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ pi I ι),
                            (fun x =>
                                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                    (_ :
                                      ∀ (a b : ι → R),
                                        Setoid.r a b →
                                          (fun f i => ↑(Quotient.mk I) (f i)) a =
                                            (fun f i => ↑(Quotient.mk I) (f i)) b))
                                (x + y) =
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  x +
                                (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case mk
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
x✝ : (ι → R) ⧸ pi I ι
x : ι → R
⊢ (fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i))
      (AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun x =>
                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                    (_ :
                      ∀ (a b : ι → R),
                        Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                map_add' :=
                  (_ :
                    ∀ (x y : (ι → R) ⧸ pi I ι),
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          (x + y) =
                        (fun x =>
                              Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                (_ :
                                  ∀ (a b : ι → R),
                                    Setoid.r a b →
                                      (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                            x +
                          (fun x =>
                              Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                (_ :
                                  ∀ (a b : ι → R),
                                    Setoid.r a b →
                                      (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                            y) },
            map_smul' :=
              (_ :
                ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                  AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      (r • x) =
                    ↑(RingHom.id (R ⧸ I)) r •
                      AddHom.toFun
                        {
                          toFun := fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                          map_add' :=
                            (_ :
                              ∀ (x y : (ι → R) ⧸ pi I ι),
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    (x + y) =
                                  (fun x =>
                                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                          (_ :
                                            ∀ (a b : ι → R),
                                              Setoid.r a b →
                                                (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                  (fun f i => ↑(Quotient.mk I) (f i)) b))
                                      x +
                                    (fun x =>
                                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                          (_ :
                                            ∀ (a b : ι → R),
                                              Setoid.r a b →
                                                (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                  (fun f i => ↑(Quotient.mk I) (f i)) b))
                                      y) }
                        x) }.toAddHom
        (Quot.mk Setoid.r x)) =
    Quot.mk Setoid.r x
[PROOFSTEP]
exact Ideal.Quotient.eq.2 fun i => Ideal.Quotient.eq.1 (Quotient.out_eq' _)
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
⊢ Function.RightInverse (fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i))
    {
          toAddHom :=
            {
              toFun := fun x =>
                Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                  (_ :
                    ∀ (a b : ι → R),
                      Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ pi I ι),
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        (x + y) =
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          x +
                        (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ pi I ι),
                            (fun x =>
                                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                    (_ :
                                      ∀ (a b : ι → R),
                                        Setoid.r a b →
                                          (fun f i => ↑(Quotient.mk I) (f i)) a =
                                            (fun f i => ↑(Quotient.mk I) (f i)) b))
                                (x + y) =
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  x +
                                (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
intro x
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
x : ι → R ⧸ I
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun x =>
                Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                  (_ :
                    ∀ (a b : ι → R),
                      Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ pi I ι),
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        (x + y) =
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          x +
                        (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ pi I ι),
                            (fun x =>
                                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                    (_ :
                                      ∀ (a b : ι → R),
                                        Setoid.r a b →
                                          (fun f i => ↑(Quotient.mk I) (f i)) a =
                                            (fun f i => ↑(Quotient.mk I) (f i)) b))
                                (x + y) =
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  x +
                                (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      x) }.toAddHom
      ((fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i)) x) =
    x
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
x : ι → R ⧸ I
i : ι
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun x =>
                Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                  (_ :
                    ∀ (a b : ι → R),
                      Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ pi I ι),
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        (x + y) =
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          x +
                        (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ pi I ι),
                            (fun x =>
                                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                    (_ :
                                      ∀ (a b : ι → R),
                                        Setoid.r a b →
                                          (fun f i => ↑(Quotient.mk I) (f i)) a =
                                            (fun f i => ↑(Quotient.mk I) (f i)) b))
                                (x + y) =
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  x +
                                (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      x) }.toAddHom
      ((fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i)) x) i =
    x i
[PROOFSTEP]
obtain ⟨_, _⟩ := @Quot.exists_rep _ _ (x i)
[GOAL]
case h.intro
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
x : ι → R ⧸ I
i : ι
w✝ : R
h✝ : Quot.mk Setoid.r w✝ = x i
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun x =>
                Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                  (_ :
                    ∀ (a b : ι → R),
                      Setoid.r a b → (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ pi I ι),
                    (fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                        (x + y) =
                      (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          x +
                        (fun x =>
                            Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                              (_ :
                                ∀ (a b : ι → R),
                                  Setoid.r a b →
                                    (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b))
                          y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ pi I ι),
                AddHom.toFun
                    {
                      toFun := fun x =>
                        Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                          (_ :
                            ∀ (a b : ι → R),
                              Setoid.r a b →
                                (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ pi I ι),
                            (fun x =>
                                  Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                    (_ :
                                      ∀ (a b : ι → R),
                                        Setoid.r a b →
                                          (fun f i => ↑(Quotient.mk I) (f i)) a =
                                            (fun f i => ↑(Quotient.mk I) (f i)) b))
                                (x + y) =
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  x +
                                (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      {
                        toFun := fun x =>
                          Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                            (_ :
                              ∀ (a b : ι → R),
                                Setoid.r a b →
                                  (fun f i => ↑(Quotient.mk I) (f i)) a = (fun f i => ↑(Quotient.mk I) (f i)) b),
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ pi I ι),
                              (fun x =>
                                    Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                      (_ :
                                        ∀ (a b : ι → R),
                                          Setoid.r a b →
                                            (fun f i => ↑(Quotient.mk I) (f i)) a =
                                              (fun f i => ↑(Quotient.mk I) (f i)) b))
                                  (x + y) =
                                (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    x +
                                  (fun x =>
                                      Quotient.liftOn' x (fun f i => ↑(Quotient.mk I) (f i))
                                        (_ :
                                          ∀ (a b : ι → R),
                                            Setoid.r a b →
                                              (fun f i => ↑(Quotient.mk I) (f i)) a =
                                                (fun f i => ↑(Quotient.mk I) (f i)) b))
                                    y) }
                      x) }.toAddHom
      ((fun x => ↑(Quotient.mk (pi I ι)) fun i => Quotient.out' (x i)) x) i =
    x i
[PROOFSTEP]
convert Quotient.out_eq' (x i)
[GOAL]
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ ↑f x i ∈ I
[PROOFSTEP]
classical
cases nonempty_fintype ι
rw [pi_eq_sum_univ x]
simp only [Finset.sum_apply, smul_eq_mul, LinearMap.map_sum, Pi.smul_apply, LinearMap.map_smul]
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)
[GOAL]
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
⊢ ↑f x i ∈ I
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f x i ∈ I
[PROOFSTEP]
rw [pi_eq_sum_univ x]
[GOAL]
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ↑f (∑ i : ι, x i • fun j => if i = j then 1 else 0) i ∈ I
[PROOFSTEP]
simp only [Finset.sum_apply, smul_eq_mul, LinearMap.map_sum, Pi.smul_apply, LinearMap.map_smul]
[GOAL]
case intro
R : Type u
inst✝¹ : CommRing R
I : Ideal R
a b : R
S ι✝ : Type v
ι : Type u_1
inst✝ : Finite ι
ι' : Type w
x : ι → R
hi : ∀ (i : ι), x i ∈ I
f : (ι → R) →ₗ[R] ι' → R
i : ι'
val✝ : Fintype ι
⊢ ∑ x_1 : ι, x x_1 * ↑f (fun j => if x_1 = j then 1 else 0) i ∈ I
[PROOFSTEP]
exact I.sum_mem fun j _ => I.mul_mem_right _ (hi j)
[GOAL]
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
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
[PROOFSTEP]
have : ∀ j ∈ s, j ≠ i → ∃ r : R, ∃ _ : r - 1 ∈ f i, r ∈ f j :=
  by
  intro j hjs hji
  specialize hf i his j hjs hji.symm
  rw [eq_top_iff_one, Submodule.mem_sup] at hf
  rcases hf with ⟨r, hri, s, hsj, hrs⟩
  refine' ⟨1 - r, _, _⟩
  · rw [sub_right_comm, sub_self, zero_sub]
    exact (f i).neg_mem hri
  · rw [← hrs, add_sub_cancel']
    exact hsj
[GOAL]
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
[PROOFSTEP]
intro j hjs hji
[GOAL]
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
[PROOFSTEP]
specialize hf i his j hjs hji.symm
[GOAL]
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
[PROOFSTEP]
rw [eq_top_iff_one, Submodule.mem_sup] at hf
[GOAL]
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
[PROOFSTEP]
rcases hf with ⟨r, hri, s, hsj, hrs⟩
[GOAL]
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
[PROOFSTEP]
refine' ⟨1 - r, _, _⟩
[GOAL]
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
[PROOFSTEP]
rw [sub_right_comm, sub_self, zero_sub]
[GOAL]
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
[PROOFSTEP]
exact (f i).neg_mem hri
[GOAL]
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
[PROOFSTEP]
rw [← hrs, add_sub_cancel']
[GOAL]
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
[PROOFSTEP]
exact hsj
[GOAL]
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
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
[PROOFSTEP]
classical
have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j :=
  by
  choose g hg1 hg2 using this
  refine' ⟨fun j => if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, fun j => _, fun j => _⟩
  · dsimp only
    split_ifs with h
    · apply hg1
    rw [sub_self]
    exact (f i).zero_mem
  · intro hjs hji
    dsimp only
    rw [dif_pos]
    · apply hg2
    exact ⟨hjs, hji⟩
rcases this with ⟨g, hgi, hgj⟩
use∏ x in s.erase i, g x
constructor
· rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, map_one, map_prod]
  apply Finset.prod_eq_one
  intros
  rw [← RingHom.map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
  apply hgi
· intro j hjs hji
  rw [← Quotient.eq_zero_iff_mem, map_prod]
  refine' Finset.prod_eq_zero (Finset.mem_erase_of_ne_of_mem hji hjs) _
  rw [Quotient.eq_zero_iff_mem]
  exact hgj j hjs hji
[GOAL]
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
⊢ ∃ r, r - 1 ∈ f i ∧ ∀ (j : ι), j ∈ s → j ≠ i → r ∈ f j
[PROOFSTEP]
have : ∃ g : ι → R, (∀ j, g j - 1 ∈ f i) ∧ ∀ j ∈ s, j ≠ i → g j ∈ f j :=
  by
  choose g hg1 hg2 using this
  refine' ⟨fun j => if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, fun j => _, fun j => _⟩
  · dsimp only
    split_ifs with h
    · apply hg1
    rw [sub_self]
    exact (f i).zero_mem
  · intro hjs hji
    dsimp only
    rw [dif_pos]
    · apply hg2
    exact ⟨hjs, hji⟩
[GOAL]
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
[PROOFSTEP]
choose g hg1 hg2 using this
[GOAL]
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
[PROOFSTEP]
refine' ⟨fun j => if H : j ∈ s ∧ j ≠ i then g j H.1 H.2 else 1, fun j => _, fun j => _⟩
[GOAL]
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
[PROOFSTEP]
dsimp only
[GOAL]
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
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
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
[PROOFSTEP]
apply hg1
[GOAL]
case neg
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
[PROOFSTEP]
rw [sub_self]
[GOAL]
case neg
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
[PROOFSTEP]
exact (f i).zero_mem
[GOAL]
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
[PROOFSTEP]
intro hjs hji
[GOAL]
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
[PROOFSTEP]
dsimp only
[GOAL]
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
[PROOFSTEP]
rw [dif_pos]
[GOAL]
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
[PROOFSTEP]
apply hg2
[GOAL]
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
[PROOFSTEP]
exact ⟨hjs, hji⟩
[GOAL]
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
[PROOFSTEP]
rcases this with ⟨g, hgi, hgj⟩
[GOAL]
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
[PROOFSTEP]
use∏ x in s.erase i, g x
[GOAL]
case 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 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
[PROOFSTEP]
constructor
[GOAL]
case h.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
[PROOFSTEP]
rw [← Ideal.Quotient.mk_eq_mk_iff_sub_mem, map_one, map_prod]
[GOAL]
case h.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
[PROOFSTEP]
apply Finset.prod_eq_one
[GOAL]
case h.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
[PROOFSTEP]
intros
[GOAL]
case h.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
[PROOFSTEP]
rw [← RingHom.map_one, Ideal.Quotient.mk_eq_mk_iff_sub_mem]
[GOAL]
case h.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
[PROOFSTEP]
apply hgi
[GOAL]
case h.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
[PROOFSTEP]
intro j hjs hji
[GOAL]
case h.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
[PROOFSTEP]
rw [← Quotient.eq_zero_iff_mem, map_prod]
[GOAL]
case h.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
[PROOFSTEP]
refine' Finset.prod_eq_zero (Finset.mem_erase_of_ne_of_mem hji hjs) _
[GOAL]
case h.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
⊢ ↑(Quotient.mk (f j)) (g j) = 0
[PROOFSTEP]
rw [Quotient.eq_zero_iff_mem]
[GOAL]
case h.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
⊢ g j ∈ f j
[PROOFSTEP]
exact hgj j hjs hji
[GOAL]
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
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
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
[PROOFSTEP]
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⟩
[GOAL]
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
[PROOFSTEP]
have := exists_sub_one_mem_and_mem (Finset.univ : Finset ι) fun i _ j _ hij => hf i j hij
[GOAL]
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
[PROOFSTEP]
choose φ hφ using this
[GOAL]
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
[PROOFSTEP]
exists fun i => φ i (Finset.mem_univ i)
[GOAL]
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
[PROOFSTEP]
exact ⟨fun i => (hφ i _).1, fun i j hij => (hφ i _).2 j (Finset.mem_univ j) hij.symm⟩
[GOAL]
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
[PROOFSTEP]
rcases this with ⟨φ, hφ1, hφ2⟩
[GOAL]
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
[PROOFSTEP]
use∑ i, g i * φ i
[GOAL]
case h
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
[PROOFSTEP]
intro i
[GOAL]
case h
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
[PROOFSTEP]
rw [← Quotient.mk_eq_mk_iff_sub_mem, map_sum]
[GOAL]
case h
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)
[PROOFSTEP]
refine' Eq.trans (Finset.sum_eq_single i _ _) _
[GOAL]
case h.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
[PROOFSTEP]
intro j _ hji
[GOAL]
case h.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
[PROOFSTEP]
rw [Quotient.eq_zero_iff_mem]
[GOAL]
case h.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
[PROOFSTEP]
exact (f i).mul_mem_left _ (hφ2 j i hji)
[GOAL]
case h.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
[PROOFSTEP]
intro hi
[GOAL]
case h.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
[PROOFSTEP]
exact (hi <| Finset.mem_univ i).elim
[GOAL]
case h.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)
[PROOFSTEP]
specialize hφ1 i
[GOAL]
case h.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)
[PROOFSTEP]
rw [← Quotient.mk_eq_mk_iff_sub_mem, RingHom.map_one] at hφ1
[GOAL]
case h.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)
[PROOFSTEP]
rw [RingHom.map_mul, hφ1, mul_one]
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
f : ι → Ideal R
r : R
hr : r ∈ ⨅ (i : ι), f i
⊢ ↑(Pi.ringHom fun i => Quotient.mk (f i)) r = 0
[PROOFSTEP]
rw [Submodule.mem_iInf] at hr
[GOAL]
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
f : ι → Ideal R
r : R
hr : ∀ (i : ι), r ∈ f i
⊢ ↑(Pi.ringHom fun i => Quotient.mk (f i)) r = 0
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
a b : R
S ι : Type v
f : ι → Ideal R
r : R
hr : ∀ (i : ι), r ∈ f i
i : ι
⊢ ↑(Pi.ringHom fun i => Quotient.mk (f i)) r i = OfNat.ofNat 0 i
[PROOFSTEP]
exact Quotient.eq_zero_iff_mem.2 (hr i)
[GOAL]
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 = ⊤
x y : R ⧸ ⨅ (i : ι), f i
r s : R
hrs : ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) = ↑(quotientInfToPiQuotient f) (Quotient.mk'' s)
i : ι
⊢ ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) i = ↑(Quotient.mk (f i)) s
[PROOFSTEP]
rw [hrs]
[GOAL]
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 = ⊤
x y : R ⧸ ⨅ (i : ι), f i
r s : R
hrs : ↑(quotientInfToPiQuotient f) (Quotient.mk'' r) = ↑(quotientInfToPiQuotient f) (Quotient.mk'' s)
i : ι
⊢ ↑(quotientInfToPiQuotient f) (Quotient.mk'' s) i = ↑(Quotient.mk (f i)) s
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
⊢ ∀ (i j : Fin 2), i ≠ j → f i ⊔ f j = ⊤
[PROOFSTEP]
intro i j h
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
i j : Fin 2
h : i ≠ j
⊢ f i ⊔ f j = ⊤
[PROOFSTEP]
fin_cases i
[GOAL]
case head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : { val := 0, isLt := (_ : 0 < 2) } ≠ j
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f j = ⊤
[PROOFSTEP]
fin_cases j
[GOAL]
case tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
j : Fin 2
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ j
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f j = ⊤
[PROOFSTEP]
fin_cases j
[GOAL]
case head.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f { val := 0, isLt := (_ : 0 < 2) } = ⊤
[PROOFSTEP]
try contradiction
[GOAL]
case head.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f { val := 0, isLt := (_ : 0 < 2) } = ⊤
[PROOFSTEP]
contradiction
[GOAL]
case head.tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } = ⊤
[PROOFSTEP]
try contradiction
[GOAL]
case head.tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } = ⊤
[PROOFSTEP]
contradiction
[GOAL]
case tail.head.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f { val := 0, isLt := (_ : 0 < 2) } = ⊤
[PROOFSTEP]
try contradiction
[GOAL]
case tail.head.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f { val := 0, isLt := (_ : 0 < 2) } = ⊤
[PROOFSTEP]
contradiction
[GOAL]
case tail.head.tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } = ⊤
[PROOFSTEP]
try contradiction
[GOAL]
case tail.head.tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } = ⊤
[PROOFSTEP]
contradiction
[GOAL]
case head.tail.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 0, isLt := (_ : 0 < 2) } ≠ { val := 1, isLt := (_ : (fun a => a < 2) 1) }
⊢ f { val := 0, isLt := (_ : 0 < 2) } ⊔ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } = ⊤
[PROOFSTEP]
assumption
[GOAL]
case tail.head.head
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
h : { val := 1, isLt := (_ : (fun a => a < 2) 1) } ≠ { val := 0, isLt := (_ : 0 < 2) }
⊢ f { val := 1, isLt := (_ : (fun a => a < 2) 1) } ⊔ f { val := 0, isLt := (_ : 0 < 2) } = ⊤
[PROOFSTEP]
rwa [sup_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
f : Fin 2 → Ideal R := ![I, J]
hf : ∀ (i j : Fin 2), i ≠ j → f i ⊔ f j = ⊤
⊢ I ⊓ J = ⨅ (i : Fin 2), f i
[PROOFSTEP]
simp [iInf, inf_comm]
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.fst (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime) =
    Quotient.factor (I ⊓ J) I (_ : I ⊓ J ≤ I)
[PROOFSTEP]
apply Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.comp (RingHom.fst (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
      (Quotient.mk (I ⊓ J)) =
    RingHom.comp (Quotient.factor (I ⊓ J) I (_ : I ⊓ J ≤ I)) (Quotient.mk (I ⊓ J))
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.fst (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
          (Quotient.mk (I ⊓ J)))
      x✝ =
    ↑(RingHom.comp (Quotient.factor (I ⊓ J) I (_ : I ⊓ J ≤ I)) (Quotient.mk (I ⊓ J))) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime) =
    Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)
[PROOFSTEP]
apply Quotient.ringHom_ext
[GOAL]
case h
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
⊢ RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
      (Quotient.mk (I ⊓ J)) =
    RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))
[PROOFSTEP]
ext
[GOAL]
case h.a
R : Type u
inst✝ : CommRing R
I✝ : Ideal R
a b : R
S : Type v
I J : Ideal R
coprime : I ⊔ J = ⊤
x✝ : R
⊢ ↑(RingHom.comp (RingHom.comp (RingHom.snd (R ⧸ I) (R ⧸ J)) ↑(quotientInfEquivQuotientProd I J coprime))
          (Quotient.mk (I ⊓ J)))
      x✝ =
    ↑(RingHom.comp (Quotient.factor (I ⊓ J) J (_ : I ⊓ J ≤ J)) (Quotient.mk (I ⊓ J))) x✝
[PROOFSTEP]
rfl