internlm/Lean-Github huggingface dataset:
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : 3 ∣ 4 * ∏ i in erase s 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Tactic:
rw [Nat.prime_three.dvd_mul] at pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : 3 ∣ 4 ∨ 3 ∣ ∏ i in erase s 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : 3 ∣ 4 ∨ 3 ∣ ∏ i in erase s 3, i
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
⊢ False
Tactic:
norm_num at pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
⊢ False
Tactic:
have : 3 ∈ s.erase 3 := by
  apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
  intro n
  simp [← hs n]
  tauto
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
this : 3 ∈ erase s 3
⊢ False
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
this : 3 ∈ erase s 3
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
⊢ 3 ∈ erase s 3
Tactic:
apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
⊢ ∀ n ∈ erase s 3, Nat.Prime n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
⊢ ∀ n ∈ erase s 3, Nat.Prime n
Tactic:
intro n
Proof state after:
n✝ : ℕ
hn : ∀ p > n✝, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
n : ℕ
⊢ n ∈ erase s 3 → Nat.Prime n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n✝ : ℕ
hn : ∀ p > n✝, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
n : ℕ
⊢ n ∈ erase s 3 → Nat.Prime n
Tactic:
simp [← hs n]
Proof state after:
n✝ : ℕ
hn : ∀ p > n✝, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
n : ℕ
⊢ ¬n = 3 → Nat.Prime n → n % 4 = 3 → Nat.Prime n
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n✝ : ℕ
hn : ∀ p > n✝, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i in erase s 3, i
n : ℕ
⊢ ¬n = 3 → Nat.Prime n → n % 4 = 3 → Nat.Prime n
Tactic:
tauto
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ 4 * ∏ i in erase s 3, i
Tactic:
apply dvd_trans _ (dvd_mul_left _ _)
Proof state after:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ ∏ i in erase s 3, i
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∣ ∏ i in erase s 3, i
Tactic:
apply dvd_prod_of_mem
Proof state after:
case ha
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∈ erase s 3
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case ha
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ p ∈ erase s 3
Tactic:
simp
Proof state after:
case ha
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ ¬p = 3 ∧ p ∈ s
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case ha
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ ¬p = 3 ∧ p ∈ s
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 3, i
⊢ p ∣ 3
Tactic:
convert Nat.dvd_sub' pdvd this
Proof state after:
case h.e'_4
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 3, i
⊢ 3 = 4 * ∏ i in erase s 3, i + 3 - 4 * ∏ i in erase s 3, i
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
case h.e'_4
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this : p ∣ 4 * ∏ i in erase s 3, i
⊢ 3 = 4 * ∏ i in erase s 3, i + 3 - 4 * ∏ i in erase s 3, i
Tactic:
simp
Proof state after:
no goals
Theorem: C05S03.primes_mod_4_eq_3_infinite
Proof state before:
n : ℕ
hn : ∀ p > n, Nat.Prime p → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), Nat.Prime p ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i in erase s 3, i + 3) % 4 = 3
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ 4 * ∏ i in erase s 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
this✝ : p ∣ 4 * ∏ i in erase s 3, i
this : p ∣ 3
⊢ p = 3
Tactic:
apply pp.eq_of_dvd_of_prime Nat.prime_three this
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:
sorry
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            := sorry
      _ = I + K*(I + J i)  := sorry
      _ = (1+K)*I + K*J i  := sorry
      _ ≤ I + K ⊓ J i      := sorry
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            := sorry
      _ = I + K*(I + J i)  := sorry
      _ = (1+K)*I + K*J i  := sorry
      _ ≤ I + K ⊓ J i      := sorry
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            := sorry
  _ = I + K*(I + J i)  := sorry
  _ = (1+K)*I + K*J i  := sorry
  _ ≤ I + K ⊓ J i      := sorry
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)
⊢ 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
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)
⊢ Surjective ↑(chineseMap I)
Tactic:
intro g
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
⊢ ∃ a, ↑(chineseMap I) a = g
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
⊢ ∃ a, ↑(chineseMap I) a = g
Tactic:
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
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
⊢ ∃ a, ↑(chineseMap I) a = g
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
⊢ ∃ 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
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
key : ∀ (i : ι), ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
⊢ ∃ a, ↑(chineseMap I) a = g
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
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
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
e : ι → R
he : ∀ (i : ι), ↑(mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) (e i) = 0
⊢ ∃ a, ↑(chineseMap I) a = g
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
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)
Proof 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
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:
sorry
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 : ι), ∃ e, ↑(mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → ↑(mk (I j)) e = 0
Tactic:
intro i
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 : ι
⊢ ∃ 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 : ι
⊢ ∃ 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
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:
sorry
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 ∈ {i}ᶜ, IsCoprime (I i) (I j)
Tactic:
sorry
Proof state after:
no goals
Theorem: my_equality
Proof state before:
a b : ℕ
⊢ a + b + a ≤ 2 * (a + b)
Tactic:
set c : ℕ := a + b
Proof state after:
a b : ℕ
c : ℕ := a + b
⊢ c + a ≤ 2 * c
Theorem: my_equality
Proof state before:
a b : ℕ
c : ℕ := a + b
⊢ c + a ≤ 2 * c
Tactic:
linarith
Proof state after:
no goals
Theorem: exercise3_1
Proof state before:
p : Prop
⊢ p ∨ ¬p
Tactic:
by_contra h
Proof state after:
p : Prop
h : ¬(p ∨ ¬p)
⊢ False
Theorem: exercise3_1
Proof state before:
p : Prop
h : ¬(p ∨ ¬p)
⊢ False
Tactic:
apply h
Proof state after:
p : Prop
h : ¬(p ∨ ¬p)
⊢ p ∨ ¬p
Theorem: exercise3_1
Proof state before:
p : Prop
h : ¬(p ∨ ¬p)
⊢ p ∨ ¬p
Tactic:
right
Proof state after:
case h
p : Prop
h : ¬(p ∨ ¬p)
⊢ ¬p
Theorem: exercise3_1
Proof state before:
case h
p : Prop
h : ¬(p ∨ ¬p)
⊢ ¬p
Tactic:
intro h2
Proof state after:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ False
Theorem: exercise3_1
Proof state before:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ False
Tactic:
apply h
Proof state after:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p ∨ ¬p
Theorem: exercise3_1
Proof state before:
case h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p ∨ ¬p
Tactic:
left
Proof state after:
case h.h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p
Theorem: exercise3_1
Proof state before:
case h.h
p : Prop
h : ¬(p ∨ ¬p)
h2 : p
⊢ p
Tactic:
assumption
Proof state after:
no goals
Theorem: exercise3_2
Proof state before:
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
have h1 : ℤ × ℕ ≃ ℕ := by exact Denumerable.eqv (ℤ × ℕ)
Proof state after:
h1 : ℤ × ℕ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Theorem: exercise3_2
Proof state before:
h1 : ℤ × ℕ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
have h2 : ℤ × ℤ ≃ ℕ := by exact Denumerable.eqv (ℤ × ℤ)
Proof state after:
h1 : ℤ × ℕ ≃ ℕ
h2 : ℤ × ℤ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Theorem: exercise3_2
Proof state before:
h1 : ℤ × ℕ ≃ ℕ
h2 : ℤ × ℤ ≃ ℕ
⊢ (ℤ × ℕ → ℤ × ℤ) ≃ (ℕ → ℕ)
Tactic:
exact Equiv.arrowCongr h1 h2
Proof state after:
no goals
Theorem: exercise3_2
Proof state before:
⊢ ℤ × ℕ ≃ ℕ
Tactic:
exact Denumerable.eqv (ℤ × ℕ)
Proof state after:
no goals
Theorem: exercise3_2
Proof state before:
h1 : ℤ × ℕ ≃ ℕ
⊢ ℤ × ℤ ≃ ℕ
Tactic:
exact Denumerable.eqv (ℤ × ℤ)
Proof state after:
no goals
Theorem: exercise3_3
Proof state before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
⊢ SequentialLimit (s ∘ r) a
Tactic:
intro ε hε
Proof state after:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Theorem: exercise3_3
Proof state before:
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs ε hε
Proof state after:
case intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Theorem: exercise3_3
Proof state before:
case intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
obtain ⟨K, hK⟩ := hr N
Proof state after:
case intro.intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Theorem: exercise3_3
Proof state before:
case intro.intro
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∃ N, ∀ n ≥ N, |(s ∘ r) n - a| < ε
Tactic:
use K
Proof state after:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∀ n ≥ K, |(s ∘ r) n - a| < ε
Theorem: exercise3_3
Proof state before:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
⊢ ∀ n ≥ K, |(s ∘ r) n - a| < ε
Tactic:
intro n hn
Proof state after:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ |(s ∘ r) n - a| < ε
Theorem: exercise3_3
Proof state before:
case h
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ |(s ∘ r) n - a| < ε
Tactic:
apply hN
Proof state after:
case h.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ r n ≥ N
Theorem: exercise3_3
Proof state before:
case h.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ r n ≥ N
Tactic:
apply hK
Proof state after:
case h.a.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ n ≥ K
Theorem: exercise3_3
Proof state before:
case h.a.a
s : ℕ → ℝ
r : ℕ → ℕ
a : ℝ
hs : SequentialLimit s a
hr : ∀ (m : ℕ), ∃ N, ∀ n ≥ N, r n ≥ m
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε
K : ℕ
hK : ∀ n ≥ K, r n ≥ N
n : ℕ
hn : n ≥ K
⊢ n ≥ K
Tactic:
assumption
Proof state after:
no goals
Theorem: exercise3_4
Proof state before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
⊢ SequentialLimit s₂ a
Tactic:
intro ε hε
Proof state after:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Theorem: exercise3_4
Proof state before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs₁ ε hε
Proof state after:
case intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Theorem: exercise3_4
Proof state before:
case intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
obtain ⟨N', hN'⟩ := hs₃ ε hε
Proof state after:
case intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε