Theorem: Int.factor_div (FltRegular/FltThree/Primes.lean)

State before:
a x : ℤ
hodd : Odd x
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
Tactic:
have h0' : x ≠ 0 := by
  rintro rfl
  contradiction
State after:
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs

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

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

case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ¬2 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs

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:
contradiction
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 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
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 : x.natAbs ≤ 2 * c.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs

State before:
case neg
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ∃ m c, c + m * x = a ∧ 2 * c.natAbs < x.natAbs
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 : x.natAbs ≤ 2 * c.natAbs
⊢ c - |x| + (a + |x|) / x * x = a

case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ 2 * (c - |x|).natAbs < x.natAbs

State before:
case neg.refine'_1
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ c - |x| + (a + |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 : x.natAbs ≤ 2 * c.natAbs
this : x ∣ |x|
⊢ c - |x| + (a + |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 : x.natAbs ≤ 2 * c.natAbs
this : x ∣ |x|
⊢ c - |x| + (a + |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 : x.natAbs ≤ 2 * c.natAbs
⊢ 2 * (c - |x|).natAbs < x.natAbs
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 : x.natAbs ≤ 2 * c.natAbs
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : x.natAbs ≤ 2 * c.natAbs
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
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 : ↑x.natAbs ≤ ↑(2 * c.natAbs)
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
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 : ↑x.natAbs ≤ ↑(2 * c.natAbs)
ofNat_two : ↑2 = 2
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ ↑(2 * c.natAbs)
ofNat_two : ↑2 = 2
⊢ ↑(2 * (c - |x|).natAbs) < ↑x.natAbs
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 : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
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 : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
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 : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * ↑c.natAbs
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
hodd : Odd x
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ 2 * ↑(c - |x|).natAbs < ↑x.natAbs
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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs < 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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs < 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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs ≠ 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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
⊢ ↑x.natAbs ≠ 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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ ¬Odd x

State before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 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 : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ 2 ∣ ↑x.natAbs

State before:
case neg.refine'_2
a x : ℤ
h0' : x ≠ 0
c : ℤ := a % x
hc : c = a % x
H : ↑x.natAbs ≤ 2 * (a % x)
ofNat_two : ↑2 = 2
hcnonneg : 0 ≤ a % x
this : a % x < |x|
heqtwomul : ↑x.natAbs = 2 * (a % x)
⊢ 2 ∣ ↑x.natAbs
Tactic:
exact ⟨_, heqtwomul⟩
State after:
no goals