Theorem: chineseMap_surj (LeanCourse/MIL/C08_Groups_and_Rings/solutions/Solutions_S02_Rings.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ Surjective ↑(chineseMap I)
Tactic:
intro g
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
⊢ ∃ a, ↑(chineseMap I) a = g

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
⊢ ∃ a, ↑(chineseMap I) a = g
Tactic:
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
⊢ ∃ a, ↑(chineseMap I) a = g

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
key : ∀ (i : ι), ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
⊢ ∃ a, ↑(chineseMap I) a = g
Tactic:
choose e he using key
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
⊢ ∃ a, ↑(chineseMap I) a = g

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
⊢ ∃ a, ↑(chineseMap I) a = g
Tactic:
use mk _ (∑ i, f i*e i)
State after:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
⊢ ↑(chineseMap I) (↑(mk (⨅ i, I i)) (∑ i : ι, f i * e i)) = g

State before:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
⊢ ↑(chineseMap I) (↑(mk (⨅ i, I i)) (∑ i : ι, f i * e i)) = g
Tactic:
ext i
State after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ↑(chineseMap I) (↑(mk (⨅ i, I i)) (∑ i : ι, f i * e i)) i = g i

State before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ↑(chineseMap I) (↑(mk (⨅ i, I i)) (∑ i : ι, f i * e i)) i = g i
Tactic:
rw [chineseMap_mk', map_sum, Fintype.sum_eq_single i]
State after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ↑(mk (I i)) (f i * e i) = g i

case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → ↑(mk (I i)) (f x * e x) = 0

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
⊢ ∀ (i : ι), ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
intro i
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
  intros j hj
  exact hI _ _ (by simpa [ne_comm, isCoprime_iff_add] using hj)
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
rcases isCoprime_iff_exists.mp (isCoprime_Inf hI') with ⟨u, hu, e, he, hue⟩
State after:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0

State before:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
State after:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0

State before:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
refine ⟨e, ?_, ?_⟩
State after:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ↑(mk (I i)) e = 1

case intro.intro.intro.intro.refine_2
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
⊢ ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
Tactic:
intros j hj
State after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ IsCoprime (I i) (I j)

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ IsCoprime (I i) (I j)
Tactic:
exact hI _ _ (by simpa [ne_comm, isCoprime_iff_add] using hj)
State after:
no goals

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ i ≠ j
Tactic:
simpa [ne_comm, isCoprime_iff_add] using hj
State after:
no goals

State before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∀ (j : ι), j ≠ i → e ∈ I j
Tactic:
simpa using he
State after:
no goals

State before:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ↑(mk (I i)) e = 1
Tactic:
simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
State after:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ↑(mk (I i)) 1 = 1

State before:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ↑(mk (I i)) 1 = 1
Tactic:
rfl
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
State after:
no goals

State before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ↑(mk (I i)) (f i * e i) = g i
Tactic:
simp [(he i).1, hf]
State after:
no goals

State before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → ↑(mk (I i)) (f x * e x) = 0
Tactic:
intros j hj
State after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ ↑(mk (I i)) (f j * e j) = 0

State before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ ↑(mk (I i)) (f j * e j) = 0
Tactic:
simp [(he j).2 i hj.symm]
State after:
no goals