internlm/Lean-Github huggingface dataset:
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) < norm y
Tactic:
have H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
Proof state after:
case H2
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y ≤ norm y / 2 * norm y

x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ norm (x % y) < norm y
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ 0 < norm y
Tactic:
rwa [norm_pos]
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
case H1
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
⊢ x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
Tactic:
ext <;> simp [Int.mod'_eq, mod_def, div_def, norm] <;> ring
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
case H2
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y ≤ norm y / 2 * norm y
Tactic:
calc
  norm (x % y) * norm y = norm (x % y * conj y) := by simp only [norm_mul, norm_conj]
  _ = |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2
      + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 := by simp [H1, norm, sq_abs]
  _ ≤ (y.norm / 2) ^ 2 + (y.norm / 2) ^ 2 := by gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
  _ = norm y / 2 * (norm y / 2 * 2) := by ring
  _ ≤ norm y / 2 * norm y := by gcongr; apply Int.ediv_mul_le; norm_num
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y) * norm y = norm (x % y * conj y)
Tactic:
simp only [norm_mul, norm_conj]
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm (x % y * conj y) =
    |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2 + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2
Tactic:
simp [H1, norm, sq_abs]
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ |Int.mod' (x.re * y.re + x.im * y.im) (norm y)| ^ 2 + |Int.mod' (-(x.re * y.im) + x.im * y.re) (norm y)| ^ 2 ≤
    (norm y / 2) ^ 2 + (norm y / 2) ^ 2
Tactic:
gcongr <;> apply Int.abs_mod'_le _ _ norm_y_pos
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ (norm y / 2) ^ 2 + (norm y / 2) ^ 2 = norm y / 2 * (norm y / 2 * 2)
Tactic:
ring
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm y / 2 * (norm y / 2 * 2) ≤ norm y / 2 * norm y
Tactic:
gcongr
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm y / 2 * 2 ≤ norm y
Theorem: gaussInt.norm_mod_lt
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ norm y / 2 * 2 ≤ norm y
Tactic:
apply Int.ediv_mul_le
Proof state after:
case h.H
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ 2 ≠ 0
Theorem: gaussInt.norm_mod_lt
Proof state before:
case h.H
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ norm y / 2 < norm y
Tactic:
apply Int.ediv_lt_of_lt_mul
Proof state after:
case H
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ 0 < 2

case H'
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ norm y < norm y * 2
Theorem: gaussInt.norm_mod_lt
Proof state before:
case H
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: gaussInt.norm_mod_lt
Proof state before:
case H'
x y : gaussInt
hy : y ≠ 0
norm_y_pos : 0 < norm y
H1 : x % y * conj y = { re := Int.mod' (x * conj y).re (norm y), im := Int.mod' (x * conj y).im (norm y) }
H2 : norm (x % y) * norm y ≤ norm y / 2 * norm y
⊢ norm y < norm y * 2
Tactic:
linarith
Proof state after:
no goals
Theorem: gaussInt.natAbs_norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ Int.natAbs (norm (x % y)) < Int.natAbs (norm y)
Tactic:
apply Int.ofNat_lt.1
Proof state after:
x y : gaussInt
hy : y ≠ 0
⊢ ↑(Int.natAbs (norm (x % y))) < ↑(Int.natAbs (norm y))
Theorem: gaussInt.natAbs_norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ ↑(Int.natAbs (norm (x % y))) < ↑(Int.natAbs (norm y))
Tactic:
simp only [Int.coe_natAbs, abs_of_nonneg, norm_nonneg]
Proof state after:
x y : gaussInt
hy : y ≠ 0
⊢ norm (x % y) < norm y
Theorem: gaussInt.natAbs_norm_mod_lt
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ norm (x % y) < norm y
Tactic:
apply norm_mod_lt x hy
Proof state after:
no goals
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
x y : gaussInt
hy : y ≠ 0
⊢ ¬Int.natAbs (norm (x * y)) < Int.natAbs (norm x)
Tactic:
apply not_lt_of_ge
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
⊢ Int.natAbs (norm (x * y)) ≥ Int.natAbs (norm x)
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
⊢ Int.natAbs (norm (x * y)) ≥ Int.natAbs (norm x)
Tactic:
rw [norm_mul, Int.natAbs_mul]
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
⊢ Int.natAbs (norm x) * Int.natAbs (norm y) ≥ Int.natAbs (norm x)
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
⊢ Int.natAbs (norm x) * Int.natAbs (norm y) ≥ Int.natAbs (norm x)
Tactic:
apply le_mul_of_one_le_right (Nat.zero_le _)
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
⊢ 1 ≤ Int.natAbs (norm y)
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
⊢ 1 ≤ Int.natAbs (norm y)
Tactic:
apply Int.ofNat_le.1
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑(Int.natAbs (norm y))
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
⊢ ↑1 ≤ ↑(Int.natAbs (norm y))
Tactic:
rw [coe_natAbs_norm]
Proof state after:
case h
x y : gaussInt
hy : y ≠ 0
⊢ ↑1 ≤ norm y
Theorem: gaussInt.not_norm_mul_left_lt_norm
Proof state before:
case h
x y : gaussInt
hy : y ≠ 0
⊢ ↑1 ≤ norm y
Tactic:
exact Int.add_one_le_of_lt ((norm_pos _).mpr hy)
Proof state after:
no goals
Theorem: chineseMap_inj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : ι → Ideal R
⊢ Injective ↑(chineseMap I)
Tactic:
rw [chineseMap, injective_lift_iff, ker_Pi_Quotient_mk]
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, IsCoprime I (J j)
⊢ IsCoprime I (⨅ j ∈ s, J j)
Tactic:
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    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 ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
s : Finset ι
hf : ∀ j ∈ s, I + J j = 1
⊢ I + ⨅ j ∈ s, J j = 1
Tactic:
induction s using Finset.induction with
| empty =>
    simp
| @insert i s _ hs =>
    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 ↦ hf j (Finset.mem_insert_of_mem hj)).symm
      _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
      _ = (1+K)*I + K*J i  := by ring
      _ ≤ I + K ⊓ J i      := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: isCoprime_Inf
Proof state before:
case insert
ι : Type u_1
R : Type u_2
inst✝ : CommRing R
I : Ideal R
J : ι → Ideal R
i : ι
s : Finset ι
a✝ : i ∉ s
hf : ∀ j ∈ insert i s, I + J j = 1
K : Ideal R := ⨅ 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 ↦ hf j (Finset.mem_insert_of_mem hj)).symm
  _ = I + K*(I + J i)  := by rw [hf i (Finset.mem_insert_self i s), mul_one]
  _ = (1+K)*I + K*J i  := by ring
  _ ≤ I + K ⊓ J i      := by gcongr ; apply mul_le_left ; apply mul_le_inf
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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
Proof 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
Theorem: chineseMap_surj
Proof 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]
Proof 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
Theorem: chineseMap_surj
Proof 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)
Proof 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
Theorem: chineseMap_surj
Proof 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⟩
Proof 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
Theorem: chineseMap_surj
Proof 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
Proof 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
Theorem: chineseMap_surj
Proof 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, ?_, ?_⟩
Proof 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
Theorem: chineseMap_surj
Proof 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
Proof 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)
Theorem: chineseMap_surj
Proof 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)
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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]
Proof 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
Theorem: chineseMap_surj
Proof 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
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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)
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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]
Proof state after:
no goals
Theorem: chineseMap_surj
Proof 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
Proof 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
Theorem: chineseMap_surj
Proof 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]
Proof state after:
no goals
Theorem: exercise1_1
Proof state before:
a b c d : ℝ
⊢ a + b + c + d = d + (b + a) + c
Tactic:
rw [add_comm a b, add_assoc d, add_comm d]
Proof state after:
no goals
Theorem: exercise1_2
Proof state before:
a b c d : ℝ
⊢ a + b + c + d = d + (b + a) + c
Tactic:
calc a + b + c + d
    = b + a + c + d := by rw [add_comm a b]
  _ = d + (b + a + c) := by rw [add_comm d]
  _ = d + (b + a) + c := by rw [add_assoc d]
Proof state after:
no goals
Theorem: exercise1_2
Proof state before:
a b c d : ℝ
⊢ a + b + c + d = b + a + c + d
Tactic:
rw [add_comm a b]
Proof state after:
no goals
Theorem: exercise1_2
Proof state before:
a b c d : ℝ
⊢ b + a + c + d = d + (b + a + c)
Tactic:
rw [add_comm d]
Proof state after:
no goals
Theorem: exercise1_2
Proof state before:
a b c d : ℝ
⊢ d + (b + a + c) = d + (b + a) + c
Tactic:
rw [add_assoc d]
Proof state after:
no goals
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a ^ 2 - b ^ 2
Tactic:
rw [pow_two a]
Proof state after:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b ^ 2
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b ^ 2
Tactic:
rw [pow_two b]
Proof state after:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ (a + b) * (a - b) = a * a - b * b
Tactic:
rw [mul_sub (a+b) a b]
Proof state after:
a b : ℝ
⊢ (a + b) * a - (a + b) * b = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ (a + b) * a - (a + b) * b = a * a - b * b
Tactic:
rw [add_mul a b a]
Proof state after:
a b : ℝ
⊢ a * a + b * a - (a + b) * b = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + b * a - (a + b) * b = a * a - b * b
Tactic:
rw [add_mul a b b]
Proof state after:
a b : ℝ
⊢ a * a + b * a - (a * b + b * b) = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + b * a - (a * b + b * b) = a * a - b * b
Tactic:
rw [mul_comm b a]
Proof state after:
a b : ℝ
⊢ a * a + a * b - (a * b + b * b) = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + a * b - (a * b + b * b) = a * a - b * b
Tactic:
rw [← sub_sub]
Proof state after:
a b : ℝ
⊢ a * a + a * b - a * b - b * b = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + a * b - a * b - b * b = a * a - b * b
Tactic:
rw [← add_sub]
Proof state after:
a b : ℝ
⊢ a * a + (a * b - a * b) - b * b = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + (a * b - a * b) - b * b = a * a - b * b
Tactic:
rw [sub_self]
Proof state after:
a b : ℝ
⊢ a * a + 0 - b * b = a * a - b * b
Theorem: exercise1_3
Proof state before:
a b : ℝ
⊢ a * a + 0 - b * b = a * a - b * b
Tactic:
rw [add_zero]
Proof state after:
no goals