Theorem: chineseMap_surj (LeanCourse/MIL/C08_Groups_and_Rings/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:
classical
intro g
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
  intro i
  have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
    sorry
  sorry
choose e he using key
use mk _ (∑ i, f i*e i)
sorry
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)
⊢ 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
⊢ ∃ a, ↑(chineseMap I) a = g
Tactic:
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
  intro i
  have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
    sorry
  sorry
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
key : ∀ (i : ι), ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 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
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:
sorry
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 : ι), ∃ 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
  sorry
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:
sorry
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 ∈ {i}ᶜ, IsCoprime (I i) (I j)
Tactic:
sorry
State after:
no goals