internlm/Lean-Github huggingface dataset:
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : Nat.succ a✝ % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0
Tactic:
rw [Nat.succ_eq_add_one] at a
Proof state after:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : (a✝ + 1) % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0
Theorem: Int.int_valuation_eq_zero_iff
Proof state before:
case mp.negSucc
R : Type u
inst : CommRing R
p : ℕ
inst_1 : IsDomain R
hp : 1 < p
a✝ : ℕ
a : (a✝ + 1) % p = 0
⊢ mod ↑(a✝ + 1) ↑p = 0
Tactic:
exact Iff.mp natAbs_eq_zero a
Proof state after:
no goals
Theorem: Int.primeVal_eq_zero_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
⊢ SurjVal.v (primeVal hp) k = 0 ↔ ¬↑p ∣ k
Tactic:
rw [primeVal, int_valuation_eq_zero_iff hp.one_lt, Int.dvd_iff_emod_eq_zero]
Proof state after:
no goals
Theorem: Int.primeVal_pos_iff
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
⊢ 0 < SurjVal.v (primeVal hp) k ↔ ↑p ∣ k
Tactic:
simp [← not_iff_not]
Proof state after:
no goals
Theorem: Int.zero_valtn_decr_p
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ decr_val_p p k = k
Tactic:
rw [decr_val_p]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ (if (k % ↑p == 0) = true then k / ↑p else k) = k
Theorem: Int.zero_valtn_decr_p
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
k : ℤ
hp : Nat.Prime p
h : SurjVal.v (primeVal hp) k = 0
⊢ (if (k % ↑p == 0) = true then k / ↑p else k) = k
Tactic:
aesop
Proof state after:
no goals
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
haveI : Fact p.Prime := ⟨hp⟩
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
by_cases this : (n : ZMod p) = 0
Proof state after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
conv_lhs =>
  rw [← show p - 1 + 1 = p from Nat.sub_add_cancel hp.one_lt.le]
Proof state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1 + 1) ≡ n [ZMOD ↑p]
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1 + 1) ≡ n [ZMOD ↑p]
Tactic:
rw [pow_add, pow_one]
Proof state after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) * n ≡ n [ZMOD ↑p]
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) * n ≡ n [ZMOD ↑p]
Tactic:
simp [← ZMod.int_cast_eq_int_cast_iff, ZMod.pow_card_sub_one_eq_one this]
Proof state after:
no goals
Theorem: Int.Int.ModEq.pow_card_eq_self
Proof state before:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
simp [← ZMod.int_cast_eq_int_cast_iff, this]
Proof state after:
no goals
Theorem: Int.val_poly_of_double_root
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
a b c : ℤ
H : has_double_root a b c hp
⊢ SurjVal.v (primeEVR hp).valtn (a * double_root a b c p ^ 2 + b * double_root a b c p + c) > 0 ∧
    SurjVal.v (primeEVR hp).valtn (2 * a * double_root a b c p + b) > 0
Tactic:
sorry
Proof state after:
no goals
Theorem: add_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
⊢ (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R
Tactic:
have : NeZero (ringChar R) := ⟨h⟩
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R
Theorem: add_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R
Tactic:
have := CharP.char_is_prime_of_pos R (ringChar R)
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R
Theorem: add_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a + b) ^ ringChar R = a ^ ringChar R + b ^ ringChar R
Tactic:
exact add_pow_char _ _ _
Proof state after:
no goals
Theorem: sub_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
have : NeZero (ringChar R) := ⟨h⟩
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Theorem: sub_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this : NeZero (ringChar R)
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
have := CharP.char_is_prime_of_pos R (ringChar R)
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Theorem: sub_pow_ringChar
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : R
h : ringChar R ≠ 0
this✝ : NeZero (ringChar R)
this : Fact (Nat.Prime (ringChar R))
⊢ (a - b) ^ ringChar R = a ^ ringChar R - b ^ ringChar R
Tactic:
exact sub_pow_char _ _ _
Proof state after:
no goals
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
⊢ Function.Injective fun x => x ^ ringChar R
Tactic:
intros x y h
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
⊢ x = y
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
⊢ x = y
Tactic:
rw [←sub_eq_zero] at *
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝ : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
⊢ x - y = 0
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝ : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
⊢ x - y = 0
Tactic:
rw [←sub_eq_zero] at *
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h✝¹ h✝ : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y - 0 = 0
⊢ x - y - 0 = 0
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : (fun x => x ^ ringChar R) x = (fun x => x ^ ringChar R) y
h✝¹ h✝ : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y = 0
h : (fun x => x ^ ringChar R) x - (fun x => x ^ ringChar R) y - 0 = 0
⊢ x - y - 0 = 0
Tactic:
simp only [sub_zero] at *
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ h : x ^ ringChar R - y ^ ringChar R = 0
⊢ x - y = 0
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ h : x ^ ringChar R - y ^ ringChar R = 0
⊢ x - y = 0
Tactic:
rw [← sub_pow_ringChar _ _ hn] at h
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ : x ^ ringChar R - y ^ ringChar R = 0
h : (x - y) ^ ringChar R = 0
⊢ x - y = 0
Theorem: pow_ringChar_injective
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
hn : ringChar R ≠ 0
x y : R
h✝² : x ^ ringChar R = y ^ ringChar R
h✝¹ h✝ : x ^ ringChar R - y ^ ringChar R = 0
h : (x - y) ^ ringChar R = 0
⊢ x - y = 0
Tactic:
exact pow_eq_zero h
Proof state after:
no goals
Theorem: factorize1
Proof state before:
R : Type u
inst✝ : CommRing R
root b p : R
q : ℕ
⊢ root * p ^ q * (p ^ q * b) + root * p ^ q * (root * p ^ q) = p ^ q * p ^ q * ((root + b) * root)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize2
Proof state before:
R : Type u
inst✝ : CommRing R
root a p : R
q : ℕ
⊢ 2 * (root * p ^ q) * (p ^ 1 * a) = p ^ q * p ^ 1 * (2 * a * root)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize3
Proof state before:
R : Type u
inst✝ : CommRing R
root p : R
q : ℕ
⊢ 3 * (root * p ^ q * (root * p ^ q)) = p ^ q * p ^ q * (3 * root * root)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize4
Proof state before:
R : Type u
inst✝ : CommRing R
root a b c p : R
q : ℕ
⊢ p ^ (2 * q + 1) * c + root * p ^ q * (p ^ (q + 1) * b) + (root * p ^ q) ^ 2 * (p ^ 1 * a) =
    p ^ q * p ^ q * p ^ 1 * (a * root ^ 2) + p ^ q * p ^ (q + 1) * (b * root) + p ^ (2 * q + 1) * c
Tactic:
ring
Proof state after:
no goals
Theorem: factorize5
Proof state before:
R : Type u
inst✝ : CommRing R
b c p : R
⊢ p ^ 1 * b * (p ^ 1 * b) + 4 * (p ^ 2 * c) = p ^ 2 * (b * b + 4 * c)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize6
Proof state before:
R : Type u
inst✝ : CommRing R
p x b c : R
⊢ p ^ 2 * x ^ 2 + p * x * (p ^ 1 * b) + p ^ 2 * -c = p ^ 2 * (1 * x ^ 2 + b * x + -c)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize7
Proof state before:
R : Type u
inst✝ : CommRing R
a b r p : R
⊢ p ^ 2 * a + 2 * (p * r) * (p ^ 1 * b) + 3 * (p * r) ^ 2 = p ^ 2 * (a + 2 * r * b + 3 * r ^ 2)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize8
Proof state before:
R : Type u
inst✝ : CommRing R
a b c r p : R
⊢ p ^ 3 * a + p * r * (p ^ 2 * b) + (p * r) ^ 2 * (p ^ 1 * c) + (p * r) ^ 3 = p ^ 3 * (a + r * b + r ^ 2 * c + r ^ 3)
Tactic:
ring
Proof state after:
no goals
Theorem: factorize9
Proof state before:
R : Type u
inst✝ : CommRing R
a1 a2 a3 a4 a6 b8 p : R
⊢ p ^ 1 * a1 * (p ^ 1 * a1) * (p ^ 3 * a6) + p ^ 1 * a1 * (p ^ 2 * a3) * -a4 + 4 * a2 * (p ^ 3 * a6) +
        a2 * (p ^ 2 * a3) * (p ^ 2 * a3) +
      p ^ 3 * -b8 =
    p ^ 3 * (p ^ 1 * a1 * (p ^ 1 * a1) * a6 + a1 * a3 * -a4 + 4 * a2 * a6 + a2 * a3 * (p ^ 1 * a3) + -b8)
Tactic:
ring
Proof state after:
no goals
Theorem: add_self_eq_mul_two
Proof state before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ a + a = 2 * a
Tactic:
rw [←one_mul a, ←add_mul, one_mul]
Proof state after:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (1 + 1) * a = 2 * a
Theorem: add_self_eq_mul_two
Proof state before:
R : Type u_1
inst✝ : Semiring R
a : R
⊢ (1 + 1) * a = 2 * a
Tactic:
congr
Proof state after:
case e_a
R : Type u_1
inst✝ : Semiring R
a : R
⊢ 1 + 1 = 2
Theorem: add_self_eq_mul_two
Proof state before:
case e_a
R : Type u_1
inst✝ : Semiring R
a : R
⊢ 1 + 1 = 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: evenpow_neg
Proof state before:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
a : R
h : n = 2 * m
⊢ (-a) ^ n = a ^ n
Tactic:
rw [h, pow_mul, pow_mul, neg_sq]
Proof state after:
no goals
Theorem: oddpow_neg
Proof state before:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
a : R
h : n = 2 * m + 1
⊢ (-a) ^ n = -a ^ n
Tactic:
rw [h, pow_succ, evenpow_neg a (show 2 * m = 2 * m by rfl), ←neg_mul_eq_neg_mul, ←pow_succ,
  Nat.add_one]
Proof state after:
no goals
Theorem: oddpow_neg
Proof state before:
R : Type u_1
inst✝ : CommRing R
n m : ℕ
a : R
h : n = 2 * m + 1
⊢ 2 * m = 2 * m
Tactic:
rfl
Proof state after:
no goals
Theorem: nzero_mul_left_cancel
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
⊢ a ≠ 0 → a * b = a * c → b = c
Tactic:
intro a_ne_z ab_eq_ac
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * b = a * c
⊢ b = c
Theorem: nzero_mul_left_cancel
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * b = a * c
⊢ b = c
Tactic:
rw [←add_left_inj (-(a * c)), add_neg_self (a * c), neg_mul_eq_mul_neg, ←mul_add] at ab_eq_ac
Proof state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
⊢ b = c
Theorem: nzero_mul_left_cancel
Proof state before:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
⊢ b = c
Tactic:
cases (@mul_eq_zero _ _ _ a (b + -c)).1 ab_eq_ac with
| inl h => exact False.elim (a_ne_z h)
| inr h =>
  rw [←add_left_inj (-c), add_neg_self c]
  exact h
Proof state after:
no goals
Theorem: nzero_mul_left_cancel
Proof state before:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : a = 0
⊢ b = c
Tactic:
exact False.elim (a_ne_z h)
Proof state after:
no goals
Theorem: nzero_mul_left_cancel
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : b + -c = 0
⊢ b = c
Tactic:
rw [←add_left_inj (-c), add_neg_self c]
Proof state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : b + -c = 0
⊢ b + -c = 0
Theorem: nzero_mul_left_cancel
Proof state before:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : R
a_ne_z : a ≠ 0
ab_eq_ac : a * (b + -c) = 0
h : b + -c = 0
⊢ b + -c = 0
Tactic:
exact h
Proof state after:
no goals
Theorem: QuadRing.gaussian_val_uniformizer
Proof state before:
p : ℕ
gt1 : 1 < p
⊢ gaussian_val p ↑p = 1
Tactic:
rw [gaussian_val]
Proof state after:
p : ℕ
gt1 : 1 < p
⊢ min (Int.int_val p (↑p).b1) (Int.int_val p (↑p).b2) = 1
Theorem: QuadRing.gaussian_val_uniformizer
Proof state before:
p : ℕ
gt1 : 1 < p
⊢ min (Int.int_val p (↑p).b1) (Int.int_val p (↑p).b2) = 1
Tactic:
simp [gt1]
Proof state after:
no goals
Theorem: QuadRing.gaussian_val_mul_eq_add
Proof state before:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a * b) = gaussian_val p a + gaussian_val p b
Tactic:
simp [gaussian_val]
Proof state after:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ min (Int.int_val p (a.b1 * b.b1 + -(a.b2 * b.b2))) (Int.int_val p (a.b2 * b.b1 + a.b1 * b.b2)) =
    min (Int.int_val p a.b1) (Int.int_val p a.b2) + min (Int.int_val p b.b1) (Int.int_val p b.b2)
Theorem: QuadRing.gaussian_val_mul_eq_add
Proof state before:
p : ℕ
prime : Nat.Prime p
a b : QuadRing ℤ 0 (-1)
⊢ min (Int.int_val p (a.b1 * b.b1 + -(a.b2 * b.b2))) (Int.int_val p (a.b2 * b.b1 + a.b1 * b.b2)) =
    min (Int.int_val p a.b1) (Int.int_val p a.b2) + min (Int.int_val p b.b1) (Int.int_val p b.b2)
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.gaussian_val_add_ge_min
Proof state before:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ gaussian_val p (a + b) ≥ min (gaussian_val p a) (gaussian_val p b)
Tactic:
simp [gaussian_val]
Proof state after:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ ((Int.int_val p a.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∧
    ((Int.int_val p a.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b2 + b.b2)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b2 + b.b2))
Theorem: QuadRing.gaussian_val_add_ge_min
Proof state before:
p : ℕ
a b : QuadRing ℤ 0 (-1)
⊢ ((Int.int_val p a.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b1 + b.b1) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b1 + b.b1)) ∧
    ((Int.int_val p a.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p a.b2 ≤ Int.int_val p (a.b2 + b.b2)) ∨
      Int.int_val p b.b1 ≤ Int.int_val p (a.b2 + b.b2) ∨ Int.int_val p b.b2 ≤ Int.int_val p (a.b2 + b.b2))
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.eq_top_of_min_eq_top
Proof state before:
a b : ℕ∞
⊢ min a b = ⊤ → a = ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.min_eq_top_iff
Proof state before:
a b : ℕ∞
⊢ min a b = ⊤ ↔ a = ⊤ ∧ b = ⊤
Tactic:
sorry
Proof state after:
no goals
Theorem: QuadRing.gaussian_val_eq_top_iff_zero
Proof state before:
p : ℕ
gt1 : 1 < p
a : QuadRing ℤ 0 (-1)
⊢ gaussian_val p a = ⊤ ↔ a = 0
Tactic:
simp [gaussian_val, gt1, QuadRing.ext_iff]
Proof state after:
no goals
Theorem: ENatValRing.key
Proof state before:
R✝ : Type u
inst✝³ : CommRing R✝
inst✝² : IsDomain R✝
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
⊢ ringChar (R ⧸ SurjVal.ideal evr.valtn) = evr.residue_char
Tactic:
sorry
Proof state after:
no goals
Theorem: v_b6_of_v_a3_a
Proof state before:
q : ℕ
h : ↑q ≥ 2
⊢ ↑q ≥ 1
Tactic:
elinarith
Proof state after:
no goals
Theorem: div_succ_le_succ_div
Proof state before:
m n : ℕ
⊢ succ m / succ n ≤ succ (m / succ n)
Tactic:
rw [succ_div]
Proof state after:
m n : ℕ
⊢ (m / succ n + if succ n ∣ m + 1 then 1 else 0) ≤ succ (m / succ n)
Theorem: div_succ_le_succ_div
Proof state before:
m n : ℕ
⊢ (m / succ n + if succ n ∣ m + 1 then 1 else 0) ≤ succ (m / succ n)
Tactic:
split
Proof state after:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)

case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Theorem: div_succ_le_succ_div
Proof state before:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)

case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
. rw [succ_eq_add_one]
Proof state after:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Theorem: div_succ_le_succ_div
Proof state before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
. rw [add_zero]
  exact le_succ (m / succ n)
Proof state after:
no goals
Theorem: div_succ_le_succ_div
Proof state before:
case inl
m n : ℕ
h✝ : succ n ∣ m + 1
⊢ m / succ n + 1 ≤ succ (m / succ n)
Tactic:
rw [succ_eq_add_one]
Proof state after:
no goals
Theorem: div_succ_le_succ_div
Proof state before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n + 0 ≤ succ (m / succ n)
Tactic:
rw [add_zero]
Proof state after:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n ≤ succ (m / succ n)
Theorem: div_succ_le_succ_div
Proof state before:
case inr
m n : ℕ
h✝ : ¬succ n ∣ m + 1
⊢ m / succ n ≤ succ (m / succ n)
Tactic:
exact le_succ (m / succ n)
Proof state after:
no goals
Theorem: div2_succ_succ_eq_succ_div2
Proof state before:
n : ℕ
⊢ succ (succ n) / 2 = succ (n / 2)
Tactic:
rw [succ_eq_add_one, succ_eq_add_one, add_assoc, add_div_eq_of_add_mod_lt, Nat.div_self (zero_lt_succ 1)]
Proof state after:
n : ℕ
⊢ n % 2 + (1 + 1) % 2 < 2
Theorem: div2_succ_succ_eq_succ_div2
Proof state before:
n : ℕ
⊢ n % 2 + (1 + 1) % 2 < 2
Tactic:
rw [mod_self, add_zero]
Proof state after:
n : ℕ
⊢ n % 2 < 2
Theorem: div2_succ_succ_eq_succ_div2
Proof state before:
n : ℕ
⊢ n % 2 < 2
Tactic:
exact mod_lt n (zero_lt_succ 1)
Proof state after:
no goals
Theorem: Int.div2_succ_le_self
Proof state before:
x : ℕ
⊢ Nat.succ x / 2 ≤ x
Tactic:
cases x with
| zero => simp
| succ x =>
  exact (div_succ_le_succ_div (Nat.succ x) 1).trans (succ_le_of_lt (div2_lt_self (succ_pos x)))
Proof state after:
no goals
Theorem: Int.div2_succ_le_self
Proof state before:
case zero

⊢ Nat.succ zero / 2 ≤ zero
Tactic:
simp
Proof state after:
no goals
Theorem: Int.div2_succ_le_self
Proof state before:
case succ
x : ℕ
⊢ Nat.succ (Nat.succ x) / 2 ≤ Nat.succ x
Tactic:
exact (div_succ_le_succ_div (Nat.succ x) 1).trans (succ_le_of_lt (div2_lt_self (succ_pos x)))
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
x : ℕ
⊢ (val_bin_nat x).snd ≤ x
Tactic:
have acc : ∀ y, y ≤ x → (val_bin_nat y).2 ≤ x := by
  induction x with
  | zero =>
    intro y h
    rw [le_zero_eq] at h
    rw [h]
    exact Nat.zero_le 0
  | succ x ih =>
    intro y y_le_sx
    cases y_le_sx with
    | refl =>
      cases mod_two_eq_zero_or_one (Nat.succ x) with
      | inl even =>
        have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
        And.intro (zero_lt_succ x) even;
        show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
        else if 0 < Nat.succ x then
        (0, Nat.succ x)
        else
        (0, 0)).snd ≤ Nat.succ x
        rw [if_pos h]
        have h' := ih (Nat.succ x / 2) (div2_succ_le_self x);
        exact le_trans h' (le_succ x)
      | inr odd =>
        show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
        let vbn_half := val_bin_nat (Nat.succ x / 2);
        (vbn_half.fst + 1, vbn_half.snd)
        else if 0 < Nat.succ x then
        (0, Nat.succ x)
        else
        (0, 0)).snd ≤ Nat.succ x
        have not_even : Nat.succ x % 2 ≠ 0 := by
          rw [odd]
          simp;
        rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
        rw [if_pos (zero_lt_succ x)]
    | step y_le_x => exact le_trans (ih y y_le_x) (le_succ x);
Proof state after:
x : ℕ
acc : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
⊢ (val_bin_nat x).snd ≤ x
Theorem: Int.odd_part_le_self_nat
Proof state before:
x : ℕ
acc : ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
⊢ (val_bin_nat x).snd ≤ x
Tactic:
exact acc x (le_refl x)
Proof state after:
no goals
Theorem: Int.odd_part_le_self_nat
Proof state before:
x : ℕ
⊢ ∀ (y : ℕ), y ≤ x → (val_bin_nat y).snd ≤ x
Tactic:
induction x with
| zero =>
  intro y h
  rw [le_zero_eq] at h
  rw [h]
  exact Nat.zero_le 0
| succ x ih =>
  intro y y_le_sx
  cases y_le_sx with
  | refl =>
    cases mod_two_eq_zero_or_one (Nat.succ x) with
    | inl even =>
      have h : 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 :=
      And.intro (zero_lt_succ x) even;
      show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
      let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then
      (0, Nat.succ x)
      else
      (0, 0)).snd ≤ Nat.succ x
      rw [if_pos h]
      have h' := ih (Nat.succ x / 2) (div2_succ_le_self x);
      exact le_trans h' (le_succ x)
    | inr odd =>
      show (if 0 < Nat.succ x ∧ Nat.succ x % 2 = 0 then
      let vbn_half := val_bin_nat (Nat.succ x / 2);
      (vbn_half.fst + 1, vbn_half.snd)
      else if 0 < Nat.succ x then
      (0, Nat.succ x)
      else
      (0, 0)).snd ≤ Nat.succ x
      have not_even : Nat.succ x % 2 ≠ 0 := by
        rw [odd]
        simp;
      rw [if_neg (not_and_of_not_right (0 < Nat.succ x) not_even)]
      rw [if_pos (zero_lt_succ x)]
  | step y_le_x => exact le_trans (ih y y_le_x) (le_succ x);
Proof state after:
no goals