internlm/Lean-Github huggingface dataset:
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2.e_s.a
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ x ∈ Finset.Icc 1 (2 * n) ∨ x ∈ Finset.Icc (2 * n + 1) (4 * n) ↔ x ∈ Finset.Icc 1 (4 * n)
Tactic:
simp only [Finset.mem_Icc]
Proof state after:
case h.e'_2.e_s.a
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n ↔ 1 ≤ x ∧ x ≤ 4 * n
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2.e_s.a.mpr
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
⊢ 1 ≤ x ∧ x ≤ 4 * n → 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
Tactic:
intros
Proof state after:
case h.e'_2.e_s.a.mpr
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
a✝ : 1 ≤ x ∧ x ≤ 4 * n
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.e'_2.e_s.a.mpr
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
a✝ : 1 ≤ x ∧ x ≤ 4 * n
⊢ 1 ≤ x ∧ x ≤ 2 * n ∨ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
Tactic:
omega
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Tactic:
apply wilson_theorem hp hn
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Disjoint (Finset.Icc 1 (2 * n)) (Finset.Icc (2 * n + 1) (4 * n))
Tactic:
rw [disjoint_iff_inf_le]
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Finset.Icc 1 (2 * n) ⊓ Finset.Icc (2 * n + 1) (4 * n) ≤ ⊥
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
⊢ Finset.Icc 1 (2 * n) ⊓ Finset.Icc (2 * n + 1) (4 * n) ≤ ⊥
Tactic:
rintro x (hx : x ∈ _ ∩ _)
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
hx : x ∈ Finset.Icc 1 (2 * n) ∩ Finset.Icc (2 * n + 1) (4 * n)
⊢ x ∈ ⊥
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
hx : x ∈ Finset.Icc 1 (2 * n) ∩ Finset.Icc (2 * n + 1) (4 * n)
⊢ x ∈ ⊥
Tactic:
rw [Finset.mem_inter, Finset.mem_Icc, Finset.mem_Icc] at hx
Proof state after:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
hx : (1 ≤ x ∧ x ≤ 2 * n) ∧ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
⊢ x ∈ ⊥
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
hx : (1 ≤ x ∧ x ≤ 2 * n) ∧ 2 * n + 1 ≤ x ∧ x ≤ 4 * n
⊢ x ∈ ⊥
Tactic:
rcases hx with ⟨⟨_, _⟩, _, _⟩
Proof state after:
case h.intro.intro.intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
left✝¹ : 1 ≤ x
right✝¹ : x ≤ 2 * n
left✝ : 2 * n + 1 ≤ x
right✝ : x ≤ 4 * n
⊢ x ∈ ⊥
Theorem: Section15Sheet7Solutions.exists_sqrt_neg_one_of_one_mod_four
Proof state before:
case h.intro.intro.intro
p : ℕ
hp : Nat.Prime p
n : ℕ
hn : p = 4 * n + 1
i : ZMod p := ∏ j in Finset.Icc 1 (2 * n), ↑j
hi : i = ∏ j in Finset.Icc 1 (2 * n), ↑j
h1 : ∏ j in Finset.Icc 1 (2 * n), -1 = 1
h2 : ∏ j in Finset.Icc 1 (2 * n), -↑j = i
h3 : ∏ j in Finset.Icc (2 * n + 1) (4 * n), ↑j = i
x : ℕ
left✝¹ : 1 ≤ x
right✝¹ : x ≤ 2 * n
left✝ : 2 * n + 1 ≤ x
right✝ : x ≤ 4 * n
⊢ x ∈ ⊥
Tactic:
linarith
Proof state after:
no goals
Theorem: Section15sheet2.int_dvd_iff
Proof state before:
x n : ℤ
hn : n ≠ 0
⊢ x ∣ n ↔ Int.natAbs x ∈ Nat.divisors (Int.natAbs n)
Tactic:
simp [hn]
Proof state after:
no goals
Theorem: Section15Sheet5Solutions.sixteen_pow_sixtyfour_mod_nineteen
Proof state before:
⊢ 16 ^ 64 = 16
Tactic:
rfl
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_thirtyseven_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 37 * a n) (37 * t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_pos_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_neg_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_const_mul
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_mul_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n * c) (t * c)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_neg'
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
simpa using tendsTo_const_mul (-1) ha
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_of_tendsTo_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
h1 : TendsTo (fun n => a n - b n) t
h2 : TendsTo b u
⊢ TendsTo a (t + u)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_sub_lim_iff
Proof state before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ TendsTo (fun n => a n - t) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_zero_mul_tendsTo_zero
Proof state before:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
⊢ TendsTo (fun n => a n * b n) 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n * b n) (t * u)
Tactic:
sorry
Proof state after:
no goals
Theorem: Section2sheet6.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
⊢ s = t
Tactic:
sorry
Proof state after:
no goals
Theorem: Ideal.mem_iff_associated
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a b : R
hab : Associated a b
⊢ a ∈ I ↔ b ∈ I
Tactic:
rcases hab with ⟨u, rfl⟩
Proof state after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a ∈ I ↔ a * ↑u ∈ I
Theorem: Ideal.mem_iff_associated
Proof state before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a ∈ I ↔ a * ↑u ∈ I
Tactic:
refine' ⟨I.mul_mem_right _, _⟩
Proof state after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a * ↑u ∈ I → a ∈ I
Theorem: Ideal.mem_iff_associated
Proof state before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
⊢ a * ↑u ∈ I → a ∈ I
Tactic:
intro h
Proof state after:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a ∈ I
Theorem: Ideal.mem_iff_associated
Proof state before:
case intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a ∈ I
Tactic:
convert I.mul_mem_right ((u⁻¹ : Rˣ) : R) h
Proof state after:
case h.e'_4
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a = a * ↑u * ↑u⁻¹
Theorem: Ideal.mem_iff_associated
Proof state before:
case h.e'_4
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
I : Ideal R
a : R
u : Rˣ
h : a * ↑u ∈ I
⊢ a = a * ↑u * ↑u⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.IsPrime.not_one_mem
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
⊢ 1 ∉ P
Tactic:
intro h
Proof state after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ False
Theorem: Ideal.IsPrime.not_one_mem
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ False
Tactic:
apply hI.ne_top
Proof state after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ P = ⊤
Theorem: Ideal.IsPrime.not_one_mem
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hI : IsPrime P
h : 1 ∈ P
⊢ P = ⊤
Tactic:
rwa [Ideal.eq_top_iff_one]
Proof state after:
no goals
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
Tactic:
refine L.induction_on ?_ ?_
Proof state after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod 0 ∈ P → ∃ x ∈ 0, x ∈ P

case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (Multiset.prod s ∈ P → ∃ x ∈ s, x ∈ P) → Multiset.prod (a ::ₘ s) ∈ P → ∃ x ∈ a ::ₘ s, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ Multiset.prod 0 ∈ P → ∃ x ∈ 0, x ∈ P
Tactic:
intro h
Proof state after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : Multiset.prod 0 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : Multiset.prod 0 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Tactic:
rw [Multiset.prod_zero] at h
Proof state after:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : 1 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_1
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
h : 1 ∈ P
⊢ ∃ x ∈ 0, x ∈ P
Tactic:
cases hP.not_one_mem h
Proof state after:
no goals
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L : Multiset R
⊢ ∀ ⦃a : R⦄ {s : Multiset R},
    (Multiset.prod s ∈ P → ∃ x ∈ s, x ∈ P) → Multiset.prod (a ::ₘ s) ∈ P → ∃ x ∈ a ::ₘ s, x ∈ P
Tactic:
intro a L IH h
Proof state after:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : Multiset.prod (a ::ₘ L) ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : Multiset.prod (a ::ₘ L) ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
simp only [Multiset.prod_cons] at h
Proof state after:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
rcases hP.mem_or_mem h with (ha | hL)
Proof state after:
case refine_2.inl
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P

case refine_2.inr
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2.inl
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
exact ⟨a, by simp, ha⟩
Proof state after:
no goals
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
ha : a ∈ P
⊢ a ∈ a ::ₘ L
Tactic:
simp
Proof state after:
no goals
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2.inr
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
obtain ⟨x, hxL, hxP⟩ := IH hL
Proof state after:
case refine_2.inr.intro.intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
x : R
hxL : x ∈ L
hxP : x ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Theorem: Ideal.IsPrime.mem_of_prod_mem
Proof state before:
case refine_2.inr.intro.intro
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
P : Ideal R
hP : IsPrime P
L✝ : Multiset R
a : R
L : Multiset R
IH : Multiset.prod L ∈ P → ∃ x ∈ L, x ∈ P
h : a * Multiset.prod L ∈ P
hL : Multiset.prod L ∈ P
x : R
hxL : x ∈ L
hxP : x ∈ P
⊢ ∃ x ∈ a ::ₘ L, x ∈ P
Tactic:
exact ⟨x, Multiset.mem_cons_of_mem hxL, hxP⟩
Proof state after:
no goals
Theorem: Prime.ideal_span_singleton_isPrime
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ Ideal.IsPrime (Ideal.span {p})
Tactic:
rwa [Ideal.span_singleton_prime]
Proof state after:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ p ≠ 0
Theorem: Prime.ideal_span_singleton_isPrime
Proof state before:
R✝ : Type
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
inst✝¹ : UniqueFactorizationMonoid R✝
R : Type
inst✝ : CommRing R
p : R
hp : Prime p
⊢ p ≠ 0
Tactic:
exact hp.ne_zero
Proof state after:
no goals
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
rw [tendsTo_def] at *
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
have h : ∀ n, |a n - t| = |-a n - -t| := by
  intro n
  rw [abs_sub_comm]
  congr 1
  ring
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
h : ∀ (n : ℕ), |a n - t| = |-a n - -t|
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
h : ∀ (n : ℕ), |a n - t| = |-a n - -t|
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |-a n - -t| < ε
Tactic:
simpa [h] using ha
Proof state after:
no goals
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
⊢ ∀ (n : ℕ), |a n - t| = |-a n - -t|
Tactic:
intro n
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |a n - t| = |-a n - -t|
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |a n - t| = |-a n - -t|
Tactic:
rw [abs_sub_comm]
Proof state after:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |t - a n| = |-a n - -t|
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ |t - a n| = |-a n - -t|
Tactic:
congr 1
Proof state after:
case e_a
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ t - a n = -a n - -t
Theorem: Section2sheet5solutions.tendsTo_neg
Proof state before:
case e_a
a : ℕ → ℝ
t : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
n : ℕ
⊢ t - a n = -a n - -t
Tactic:
ring
Proof state after:
no goals
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n + b n) (t + u)
Tactic:
rw [tendsTo_def] at *
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
intro ε hε
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
specialize ha (ε / 2) (by linarith)
Proof state after:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Theorem: Section2sheet5solutions.tendsTo_add
Proof state before:
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
ha : ∃ B, ∀ (n : ℕ), B ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε
Tactic:
cases' ha with X hX
Proof state after:
case intro
a b : ℕ → ℝ
t u : ℝ
hb : ∀ (ε : ℝ), 0 < ε → ∃ B, ∀ (n : ℕ), B ≤ n → |b n - u| < ε
ε : ℝ
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / 2
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |a n + b n - (t + u)| < ε