Theorem: HW2.problem_3 (BrownCs22/Homework/Hw2sols.lean)

State before:
⊢ ∀ (x : ℕ), x ∣ 10 → x ∣ 100
Tactic:
intro x
State after:
x : ℕ
⊢ x ∣ 10 → x ∣ 100

State before:
x : ℕ
⊢ x ∣ 10 → x ∣ 100
Tactic:
intro hxdvd
State after:
x : ℕ
hxdvd : x ∣ 10
⊢ x ∣ 100

State before:
x : ℕ
hxdvd : x ∣ 10
⊢ x ∣ 100
Tactic:
dsimp [dvd] at hxdvd
State after:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ x ∣ 100

State before:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ x ∣ 100
Tactic:
dsimp [dvd]
State after:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ ∃ c, 100 = x * c

State before:
x : ℕ
hxdvd : ∃ c, 10 = x * c
⊢ ∃ c, 100 = x * c
Tactic:
eliminate hxdvd with k hkx
State after:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ ∃ c, 100 = x * c

State before:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ ∃ c, 100 = x * c
Tactic:
existsi k*10
State after:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ 100 = x * (k * 10)

State before:
case intro
x k : ℕ
hkx : 10 = x * k
⊢ 100 = x * (k * 10)
Tactic:
linarith
State after:
no goals