internlm/Lean-Github huggingface dataset:
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case intro
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ |(u ∘ φ) n - l| ≤ ε
Tactic:
apply hN
Proof state after:
case intro.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Theorem: subseq_tendsto_of_tendsto'
Proof state before:
case intro.a
u : ℕ → ℝ
l : ℝ
φ : ℕ → ℕ
h : seq_limit u l
hφ : extraction φ
ε : ℝ
ε_pos : ε > 0
N : ℕ
hN : ∀ n ≥ N, |u n - l| ≤ ε
n : ℕ
hn : n ≥ N
⊢ φ n ≥ N
Tactic:
calc
  N ≤ n := hn
  _ ≤ φ n := id_le_extraction' hφ n
Proof state after:
no goals
Theorem: cluster_limit
Proof state before:
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
ha : cluster_point u a
⊢ a = l
Tactic:
rcases ha with ⟨φ, φ_extr, lim_u_φ⟩
Proof state after:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
⊢ a = l
Theorem: cluster_limit
Proof state before:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
⊢ a = l
Tactic:
have lim_u_φ' : seq_limit (u ∘ φ) l := subseq_tendsto_of_tendsto' hl φ_extr
Proof state after:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
lim_u_φ' : seq_limit (u ∘ φ) l
⊢ a = l
Theorem: cluster_limit
Proof state before:
case intro.intro
u : ℕ → ℝ
l a : ℝ
hl : seq_limit u l
φ : ℕ → ℕ
φ_extr : extraction φ
lim_u_φ : seq_limit (u ∘ φ) a
lim_u_φ' : seq_limit (u ∘ φ) l
⊢ a = l
Tactic:
exact unique_limit lim_u_φ lim_u_φ'
Proof state after:
no goals
Theorem: Ideal.ker_Pi_Quotient_mk
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : ι → Ideal R
⊢ ker (Pi.ringHom fun i => Quotient.mk (I i)) = ⨅ (i : ι), I i
Tactic:
simp [Pi.ker_ringHom, Ideal.ker_mk]
Proof state after:
no goals
Theorem: Ideal.chineseMap_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : ι → Ideal R
⊢ Injective ↑(chineseMap I)
Tactic:
rw [chineseMap, injective_lift_iff, ker_Pi_Quotient_mk]
Proof state after:
no goals
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
Tactic:
revert hf
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
⊢ (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
s : Finset ι
⊢ (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
Tactic:
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    intro h
    rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
    set K := ⨅ j ∈ s, J j
    calc
      1 = I + K            := (hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [h i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf
Proof state after:
no goals
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
case empty
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
⊢ (∀ j ∈ ∅, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ ∅), J j = 1
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
⊢ (∀ j ∈ insert i s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
Tactic:
intro h
Proof state after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ I + ⨅ (j : ι) (_ : j ∈ insert i s), J j = 1
Tactic:
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
Proof state after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ (x : ι) (_ : x ∈ s), J x) ⊓ J i
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
hs : (∀ j ∈ s, I + J j = 1) → I + ⨅ (j : ι) (_ : j ∈ s), J j = 1
h : ∀ j ∈ insert i s, I + J j = 1
⊢ 1 ≤ I + (⨅ (x : ι) (_ : x ∈ s), J x) ⊓ J i
Tactic:
set K := ⨅ j ∈ s, J j
Proof state after:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
case insert
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ 1 ≤ I + K ⊓ J i
Tactic:
calc
  1 = I + K            := (hs fun j hj ↦ h j (Finset.mem_insert_of_mem hj)).symm
  _ = I + K*(I + J i)  := by rw [h i (Finset.mem_insert_self i s), mul_one]
  _ = (1+K)*I + K*J i  := by ring
  _ ≤ I + K ⊓ J i      := add_le_add mul_le_left mul_le_inf
Proof state after:
no goals
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K = I + K * (I + J i)
Tactic:
rw [h i (Finset.mem_insert_self i s), mul_one]
Proof state after:
no goals
Theorem: Ideal.coprime_iInf_of_coprime
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
ι : Type
inst✝ : DecidableEq ι
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : ¬i ∈ s
h : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ (j : ι) (_ : j ∈ s), J j
hs : (∀ j ∈ s, I + J j = 1) → I + K = 1
⊢ I + K * (I + J i) = (1 + K) * I + K * J i
Tactic:
ring
Proof state after:
no goals
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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)
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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)
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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]
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
}
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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⟩
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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, ?_, ?_⟩
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof state after:
no goals
Theorem: Ideal.chineseMap_surjective
Proof 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]
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof state after:
no goals
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof state after:
no goals
Theorem: Ideal.chineseMap_surjective
Proof 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]
Proof state after:
no goals
Theorem: Ideal.chineseMap_surjective
Proof 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
Proof 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
Theorem: Ideal.chineseMap_surjective
Proof 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]
Proof state after:
no goals