Theorem: le_abs_of_dvd (FormalBook/Chapter_06.lean)

State before:
i j : ℤ
gj : 0 ≠ j
h : i ∣ j
⊢ |i| ≤ |j|
Tactic:
dsimp [Dvd.dvd] at h
State after:
i j : ℤ
gj : 0 ≠ j
h : ∃ c, j = i * c
⊢ |i| ≤ |j|

State before:
i j : ℤ
gj : 0 ≠ j
h : ∃ c, j = i * c
⊢ |i| ≤ |j|
Tactic:
cases' h with c h₀
State after:
case intro
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
⊢ |i| ≤ |j|

State before:
case intro
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
⊢ |i| ≤ |j|
Tactic:
cases' em (c = 0) with hc h
State after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
⊢ |i| ≤ |j|

case intro.inr
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |j|

State before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
⊢ |i| ≤ |j|
Tactic:
by_contra
State after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False

State before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Tactic:
rw [hc] at h₀
State after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * 0
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False

State before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * 0
hc : c = 0
x✝ : ¬|i| ≤ |j|
⊢ False
Tactic:
simp only [mul_zero] at h₀
State after:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
hc : c = 0
x✝ : ¬|i| ≤ |j|
h₀ : j = 0
⊢ False

State before:
case intro.inl
i j : ℤ
gj : 0 ≠ j
c : ℤ
hc : c = 0
x✝ : ¬|i| ≤ |j|
h₀ : j = 0
⊢ False
Tactic:
exact gj (Eq.symm h₀)
State after:
no goals

State before:
case intro.inr
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |j|
Tactic:
calc
  |i| ≤ (|i|)*|c| := by
      exact le_mul_of_le_of_one_le' rfl.ge (Int.one_le_abs h) (abs_nonneg c) (abs_nonneg i)
    _ = |i*c| := Eq.symm (abs_mul i c)
    _ = |j| := by rw [Eq.symm h₀]
State after:
no goals

State before:
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i| ≤ |i| * |c|
Tactic:
exact le_mul_of_le_of_one_le' rfl.ge (Int.one_le_abs h) (abs_nonneg c) (abs_nonneg i)
State after:
no goals

State before:
i j : ℤ
gj : 0 ≠ j
c : ℤ
h₀ : j = i * c
h : ¬c = 0
⊢ |i * c| = |j|
Tactic:
rw [Eq.symm h₀]
State after:
no goals