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

State before:
⊢ ∀ (b a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
by_strong_induc
State after:
⊢ ∀ (b : ℕ), (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b

State before:
⊢ ∀ (b : ℕ), (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
fix b : Nat
State after:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b

State before:
b : ℕ
⊢ (∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1) → ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1
State after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
⊢ ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b

State before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
⊢ ∀ (a : ℕ), gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
fix a : Nat
State after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

State before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
by_cases h1 : b = 0
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
rewrite [h1, gcd_base]
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ a ∧ a ∣ 0

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ a ∧ a ∣ 0
Tactic:
apply And.intro (dvd_self a)
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ 0

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ a ∣ 0
Tactic:
define
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ ∃ c, 0 = a * c

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ ∃ c, 0 = a * c
Tactic:
apply Exists.intro 0
State after:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ 0 = a * 0

State before:
case pos
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : b = 0
⊢ 0 = a * 0
Tactic:
rfl
State after:
no goals

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd a b ∣ a ∧ gcd a b ∣ b
Tactic:
rewrite [gcd_nonzero a h1]
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
have h2 : a % b < b := mod_nonzero_lt a h1
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=
  ih (a % b) h2 b
State after:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b

State before:
case neg
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
Tactic:
apply And.intro _ h3.left
State after:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a

State before:
b : ℕ
ih : ∀ b_1 < b, ∀ (a : ℕ), gcd a b_1 ∣ a ∧ gcd a b_1 ∣ b_1
a : ℕ
h1 : ¬b = 0
h2 : a % b < b
h3 : gcd b (a % b) ∣ b ∧ gcd b (a % b) ∣ a % b
⊢ gcd b (a % b) ∣ a
Tactic:
show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right
State after:
no goals