internlm/Lean-Github huggingface dataset:
Theorem: even_and_odd_factors'
Proof state before:
x : ℤ
⊢ UniqueFactorizationMonoid.normalizedFactors x = Multiset.replicate (evenFactorExp x) 2 + oddFactors x
Tactic:
convert even_and_odd_factors'' x
Proof state after:
case h.e'_3.h.e'_5
x : ℤ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)
Theorem: even_and_odd_factors'
Proof state before:
case h.e'_3.h.e'_5
x : ℤ
⊢ Multiset.replicate (evenFactorExp x) 2 = Multiset.filter (Eq 2) (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
simp [evenFactorExp, ← Multiset.filter_eq]
Proof state after:
no goals
Theorem: even_and_oddFactors
Proof state before:
x : ℤ
hx : x ≠ 0
⊢ Associated x (2 ^ evenFactorExp x * Multiset.prod (oddFactors x))
Tactic:
convert(UniqueFactorizationMonoid.normalizedFactors_prod hx).symm
Proof state after:
case h.e'_4
x : ℤ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * Multiset.prod (oddFactors x) = Multiset.prod (UniqueFactorizationMonoid.normalizedFactors x)
Theorem: even_and_oddFactors
Proof state before:
case h.e'_4
x : ℤ
hx : x ≠ 0
⊢ 2 ^ evenFactorExp x * Multiset.prod (oddFactors x) = Multiset.prod (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
simp [evenFactorExp]
Proof state after:
case h.e'_4
x : ℤ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * Multiset.prod (oddFactors x) =
    Multiset.prod (UniqueFactorizationMonoid.normalizedFactors x)
Theorem: even_and_oddFactors
Proof state before:
case h.e'_4
x : ℤ
hx : x ≠ 0
⊢ 2 ^ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) * Multiset.prod (oddFactors x) =
    Multiset.prod (UniqueFactorizationMonoid.normalizedFactors x)
Tactic:
rw [Multiset.pow_count, ← Multiset.prod_add, ← even_and_odd_factors'' x]
Proof state after:
no goals
Theorem: factors_2_even
Proof state before:
z : ℤ
hz : z ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₀ : (4 : ℤ) ≠ 0 := four_ne_zero
Proof state after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Theorem: factors_2_even
Proof state before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
have h₁ : (2 : Int) ^ 2 = 4 := by norm_num
Proof state after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Theorem: factors_2_even
Proof state before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ evenFactorExp (4 * z) = 2 + evenFactorExp z
Tactic:
simp [evenFactorExp]
Proof state after:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Theorem: factors_2_even
Proof state before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
h₁ : 2 ^ 2 = 4
⊢ Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors (4 * z)) =
    2 + Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors z)
Tactic:
rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁,
  UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul,
  UniqueFactorizationMonoid.normalizedFactors_irreducible Int.prime_two.irreducible,
  Int.normalize_of_nonneg zero_le_two, Multiset.count_singleton_self, mul_one]
Proof state after:
no goals
Theorem: factors_2_even
Proof state before:
z : ℤ
hz : z ≠ 0
h₀ : 4 ≠ 0
⊢ 2 ^ 2 = 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.nonneg
Proof state before:
z a : ℤ
ha : a ∈ factorsOddPrimeOrFour z
⊢ 0 ≤ a
Tactic:
simp only [factorsOddPrimeOrFour, Multiset.mem_add] at ha
Proof state after:
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4 ∨ a ∈ oddFactors z
⊢ 0 ≤ a
Theorem: factorsOddPrimeOrFour.nonneg
Proof state before:
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4 ∨ a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
cases ha with
| inl ha =>
  rw [Multiset.eq_of_mem_replicate ha]
  norm_num
| inr ha =>
  exact oddFactors.nonneg ha
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.nonneg
Proof state before:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ a
Tactic:
rw [Multiset.eq_of_mem_replicate ha]
Proof state after:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ 4
Theorem: factorsOddPrimeOrFour.nonneg
Proof state before:
case inl
z a : ℤ
ha : a ∈ Multiset.replicate (evenFactorExp z / 2) 4
⊢ 0 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.nonneg
Proof state before:
case inr
z a : ℤ
ha : a ∈ oddFactors z
⊢ 0 ≤ a
Tactic:
exact oddFactors.nonneg ha
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Multiset.prod (factorsOddPrimeOrFour a) = a
Tactic:
apply Int.eq_of_associated_of_nonneg
Proof state after:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a

case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)

case hb
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ a
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
Tactic:
have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne'
Proof state after:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) a
Tactic:
apply Associated.trans _ this
Proof state after:
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
Tactic:
obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven
Proof state after:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (Multiset.prod (factorsOddPrimeOrFour a)) (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a))
Tactic:
rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm,
  Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul]
Proof state after:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (4 ^ m * Multiset.prod (oddFactors a)) ((2 ^ 2) ^ m * Multiset.prod (oddFactors a))
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case intro
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
this : Associated (Multiset.prod (UniqueFactorizationMonoid.normalizedFactors a)) a
m : ℕ
hm : evenFactorExp a = 2 * m
⊢ Associated (4 ^ m * Multiset.prod (oddFactors a)) ((2 ^ 2) ^ m * Multiset.prod (oddFactors a))
Tactic:
exact Associated.refl _
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case ha
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ Multiset.prod (factorsOddPrimeOrFour a)
Tactic:
apply Multiset.prod_nonneg
Proof state after:
case ha.h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ ∀ (a_1 : ℤ), a_1 ∈ factorsOddPrimeOrFour a → 0 ≤ a_1
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case ha.h
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ ∀ (a_1 : ℤ), a_1 ∈ factorsOddPrimeOrFour a → 0 ≤ a_1
Tactic:
apply factorsOddPrimeOrFour.nonneg
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.prod'
Proof state before:
case hb
a : ℤ
ha : 0 < a
heven : Even (evenFactorExp a)
⊢ 0 ≤ a
Tactic:
exact ha.le
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel Associated f (factorsOddPrimeOrFour a)
Tactic:
apply factors_unique_prod' hf
Proof state after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (x : ℤ), x ∈ factorsOddPrimeOrFour a → OddPrimeOrFour x

case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Associated (Multiset.prod f) (Multiset.prod (factorsOddPrimeOrFour a))
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (x : ℤ), x ∈ factorsOddPrimeOrFour a → OddPrimeOrFour x
Tactic:
intro x hx
Proof state after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ factorsOddPrimeOrFour a
⊢ OddPrimeOrFour x
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ factorsOddPrimeOrFour a
⊢ OddPrimeOrFour x
Tactic:
simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx
Proof state after:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ OddPrimeOrFour x
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ OddPrimeOrFour x
Tactic:
apply Or.imp _ _ hx
Proof state after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ Multiset.replicate (evenFactorExp a / 2) 4 → x = 4

a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ oddFactors a → Prime x ∧ Odd x
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ Multiset.replicate (evenFactorExp a / 2) 4 → x = 4
Tactic:
exact Multiset.eq_of_mem_replicate
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ oddFactors a → Prime x ∧ Odd x
Tactic:
simp only [oddFactors, Multiset.mem_filter]
Proof state after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Odd x → Prime x ∧ Odd x
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ Multiset.replicate (evenFactorExp a / 2) 4 ∨ x ∈ oddFactors a
⊢ x ∈ UniqueFactorizationMonoid.normalizedFactors a ∧ Odd x → Prime x ∧ Odd x
Tactic:
exact And.imp_left (UniqueFactorizationMonoid.prime_of_normalized_factor _)
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.associated'
Proof state before:
case a
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Associated (Multiset.prod f) (Multiset.prod (factorsOddPrimeOrFour a))
Tactic:
rwa [factorsOddPrimeOrFour.prod' ha heven]
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ f = factorsOddPrimeOrFour a
Tactic:
rw [← Multiset.rel_eq]
Proof state after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel (fun x x_1 => x = x_1) f (factorsOddPrimeOrFour a)
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ Multiset.Rel (fun x x_1 => x = x_1) f (factorsOddPrimeOrFour a)
Tactic:
apply Multiset.Rel.mono (factorsOddPrimeOrFour.associated' hf ha heven hassoc)
Proof state after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (a_1 : ℤ), a_1 ∈ f → ∀ (b : ℤ), b ∈ factorsOddPrimeOrFour a → Associated a_1 b → a_1 = b
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
⊢ ∀ (a_1 : ℤ), a_1 ∈ f → ∀ (b : ℤ), b ∈ factorsOddPrimeOrFour a → Associated a_1 b → a_1 = b
Tactic:
intro x hx y hy hxy
Proof state after:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ f
y : ℤ
hy : y ∈ factorsOddPrimeOrFour a
hxy : Associated x y
⊢ x = y
Theorem: factorsOddPrimeOrFour.unique'
Proof state before:
a : ℤ
f : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x
hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x
ha : 0 < a
heven : Even (evenFactorExp a)
hassoc : Associated (Multiset.prod f) a
x : ℤ
hx : x ∈ f
y : ℤ
hy : y ∈ factorsOddPrimeOrFour a
hxy : Associated x y
⊢ x = y
Tactic:
exact Int.eq_of_associated_of_nonneg hxy (hf' x hx) (factorsOddPrimeOrFour.nonneg hy)
Proof state after:
no goals
Theorem: factorsOddPrimeOrFour.pow
Proof state before:
z : ℤ
n : ℕ
hz : Even (evenFactorExp z)
⊢ factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z
Tactic:
simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow,
  Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow]
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
have h0' : x ≠ 0 := by
  rintro rfl
  simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
Proof state after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
set c := a % x with hc
Proof state after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Theorem: Int.factor_div
Proof state before:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
by_cases H : 2 * c.natAbs < x.natAbs
Proof state after:
case pos
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : 2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x

case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Theorem: Int.factor_div
Proof state before:
a : ℤ
hodd : Odd 0
⊢ False
Tactic:
simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case pos
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : 2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * natAbs c < natAbs x
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
push_neg  at H
Proof state after:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Theorem: Int.factor_div
Proof state before:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x
Tactic:
refine' ⟨(a + abs x) / x, c - abs x, _, _⟩
Proof state after:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ c - abs x + (a + abs x) / x * x = a

case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ 2 * natAbs (c - abs x) < natAbs x
Theorem: Int.factor_div
Proof state before:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ c - abs x + (a + abs x) / x * x = a
Tactic:
have := self_dvd_abs x
Proof state after:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
this : x ∣ abs x
⊢ c - abs x + (a + abs x) / x * x = a
Theorem: Int.factor_div
Proof state before:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
this : x ∣ abs x
⊢ c - abs x + (a + abs x) / x * x = a
Tactic:
rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc,
  Int.emod_add_ediv']
Proof state after:
no goals
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ 2 * natAbs (c - abs x) < natAbs x
Tactic:
rw [← Int.ofNat_lt]
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : natAbs x ≤ 2 * natAbs (a % x)
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
replace H := Int.ofNat_le_ofNat_of_le H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ ↑(2 * natAbs (a % x))
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ ↑(2 * natAbs (a % x))
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
have ofNat_two : ((2 : Nat) : Int) = 2 := rfl
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ ↑(2 * natAbs (a % x))
ofNat_two : ↑2 = 2
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ ↑(2 * natAbs (a % x))
ofNat_two : ↑2 = 2
⊢ ↑(2 * natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
rw [Int.ofNat_mul, ofNat_two] at H⊢
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
have hcnonneg := Int.emod_nonneg a h0'
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
have := Int.emod_lt a h0'
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * ↑(natAbs (a % x))
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
rw [Int.natAbs_of_nonneg hcnonneg] at H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ 2 * ↑(natAbs (c - abs x)) < ↑(natAbs x)
Tactic:
rw [← Int.natAbs_neg, neg_sub, Int.natAbs_of_nonneg (sub_nonneg_of_le this.le), mul_sub,
  sub_lt_iff_lt_add, two_mul, Int.abs_eq_natAbs, add_lt_add_iff_left]
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ ↑(natAbs x) < 2 * (a % x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ ↑(natAbs x) < 2 * (a % x)
Tactic:
apply lt_of_le_of_ne H
Proof state after:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ ↑(natAbs x) ≠ 2 * (a % x)
Theorem: Int.factor_div
Proof state before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
⊢ ↑(natAbs x) ≠ 2 * (a % x)
Tactic:
contrapose! hodd with heqtwomul
Proof state after:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑(natAbs x) ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < abs x
heqtwomul : ↑(natAbs x) = 2 * (a % x)
⊢ ¬Odd x