Theorem: HTPI.dvd_trans (HTPILib/Chap7.lean)

State before:
a b c : ℕ
h1 : a ∣ b
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h1
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : b ∣ c
⊢ a ∣ c
Tactic:
define at h2
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ a ∣ c
Tactic:
define
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (m : Nat) (h3 : b = a * m) from h1
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
⊢ ∃ c_1, c = a * c_1
Tactic:
obtain (n : Nat) (h4 : c = b * n) from h2
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = b * n
⊢ ∃ c_1, c = a * c_1
Tactic:
rewrite [h3, mul_assoc] at h4
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ ∃ c_1, c = a * c_1

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ ∃ c_1, c = a * c_1
Tactic:
apply Exists.intro (m * n)
State after:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ c = a * (m * n)

State before:
a b c : ℕ
h1 : ∃ c, b = a * c
h2 : ∃ c_1, c = b * c_1
m : ℕ
h3 : b = a * m
n : ℕ
h4 : c = a * (m * n)
⊢ c = a * (m * n)
Tactic:
show c = a * (m * n) from h4
State after:
no goals