Theorem: Ideal.chineseMap_surjective (LCTutorial/Solutions/Topics/ChineseRemainder.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ I i + I j = 1
Tactic:
apply hI
State after:
case a
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ i ≠ j

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

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

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

State before:
case intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ (j : ι) (_ : j ∈ {i}ᶜ), I j
hue : u + e = 1
⊢ ∀ (j : ι), j ≠ i → ↑(Quotient.mk (I j)) e = 0
Tactic:
intros j hj
State after:
case intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ (j : ι) (_ : j ∈ {i}ᶜ), I j
hue : u + e = 1
j : ι
hj : j ≠ i
⊢ ↑(Quotient.mk (I j)) e = 0

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

State before:
case intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ (j : ι) (_ : j ∈ {i}ᶜ), I j
hue : u + e = 1
j : ι
hj : j ≠ i
⊢ e ∈ I j
Tactic:
simp at he
State after:
case intro.intro.intro.intro.refine_2
R : Type u_1
inst✝² : CommRing R
ι : Type
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → I i + I j = 1
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), ↑(Quotient.mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, I i + I j = 1
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
j : ι
hj : j ≠ i
he : ∀ (i_1 : ι), ¬i_1 = i → e ∈ I i_1
⊢ e ∈ I j

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

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

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

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