Theorem: HTPI.Theorem_3_3_7 (HTPILib/Chap3.lean)

State before:
⊢ ∀ (a b c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix a : Int
State after:
a : ℤ
⊢ ∀ (b c : ℤ), a ∣ b → b ∣ c → a ∣ c

State before:
a : ℤ
⊢ ∀ (b c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix b : Int
State after:
a b : ℤ
⊢ ∀ (c : ℤ), a ∣ b → b ∣ c → a ∣ c

State before:
a b : ℤ
⊢ ∀ (c : ℤ), a ∣ b → b ∣ c → a ∣ c
Tactic:
fix c : Int
State after:
a b c : ℤ
⊢ a ∣ b → b ∣ c → a ∣ c

State before:
a b c : ℤ
⊢ a ∣ b → b ∣ c → a ∣ c
Tactic:
assume h1 : a ∣ b
State after:
a b c : ℤ
h1 : a ∣ b
⊢ b ∣ c → a ∣ c

State before:
a b c : ℤ
h1 : a ∣ b
⊢ b ∣ c → a ∣ c
Tactic:
assume h2 : b ∣ c
State after:
a b c : ℤ
h1 : a ∣ b
h2 : b ∣ c
⊢ a ∣ c

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 : Int) (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 : Int) (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] 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:
rewrite [mul_assoc a m n] 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 = 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