Theorem: HTPI.Lemma_7_4_7_aux (HTPILib/Chap8Part2.lean)

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b ≡ ↑a (MOD m)
Tactic:
define
State after:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ ∃ c, t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * c

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ ∃ c, t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * c
Tactic:
apply Exists.intro (s * (b - a))
State after:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * (s * (↑b - ↑a))

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = ↑m * (s * (↑b - ↑a))
Tactic:
show t * n * a + s * m * b - a = m * (s * (b - a)) from
  calc t * n * a + s * m * b - a
    _ = (t * n - 1) * a + s * m * b := by ring
    _ = (t * n - (s * m + t * n)) * a + s * m * b := by rw [h]
    _ = m * (s * (b - a)) := by ring
State after:
no goals

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ t * ↑n * ↑a + s * ↑m * ↑b - ↑a = (t * ↑n - 1) * ↑a + s * ↑m * ↑b
Tactic:
ring
State after:
no goals

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ (t * ↑n - 1) * ↑a + s * ↑m * ↑b = (t * ↑n - (s * ↑m + t * ↑n)) * ↑a + s * ↑m * ↑b
Tactic:
rw [h]
State after:
no goals

State before:
m n : ℕ
s t : ℤ
h : s * ↑m + t * ↑n = 1
a b : ℕ
⊢ (t * ↑n - (s * ↑m + t * ↑n)) * ↑a + s * ↑m * ↑b = ↑m * (s * (↑b - ↑a))
Tactic:
ring
State after:
no goals