Theorem: Int.factor_div (Flt/Primes.lean)

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
State after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * natAbs c < natAbs x

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
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

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
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

State before:
a x : ℤ
hodd : Odd x
⊢ x ≠ 0
Tactic:
rintro rfl
State after:
a : ℤ
hodd : Odd 0
⊢ False

State before:
a : ℤ
hodd : Odd 0
⊢ False
Tactic:
simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
State after:
no goals

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⟩
State after:
no goals

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
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

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, _, _⟩
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

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
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

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']
State after:
no goals

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]
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)

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
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)

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
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)

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⊢
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)

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'
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)

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'
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)

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
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)

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]
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)

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
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)

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
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

State before:
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
Tactic:
rw [← Int.even_iff_not_odd, ← Int.natAbs_even, ← Int.even_coe_nat, even_iff_two_dvd]
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)
⊢ 2 ∣ ↑(natAbs x)

State before:
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)
⊢ 2 ∣ ↑(natAbs x)
Tactic:
exact ⟨_, heqtwomul⟩
State after:
no goals