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

State before:
m : ℕ
⊢ ∀ {a b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
fix a : Int
State after:
m : ℕ
a : ℤ
⊢ ∀ {b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)

State before:
m : ℕ
a : ℤ
⊢ ∀ {b : ℤ}, a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
fix b : Int
State after:
m : ℕ
a b : ℤ
⊢ a ≡ b (MOD m) → b ≡ a (MOD m)

State before:
m : ℕ
a b : ℤ
⊢ a ≡ b (MOD m) → b ≡ a (MOD m)
Tactic:
assume h1 : a ≡ b (MOD m)
State after:
m : ℕ
a b : ℤ
h1 : a ≡ b (MOD m)
⊢ b ≡ a (MOD m)

State before:
m : ℕ
a b : ℤ
h1 : a ≡ b (MOD m)
⊢ b ≡ a (MOD m)
Tactic:
define at h1
State after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ b ≡ a (MOD m)

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ b ≡ a (MOD m)
Tactic:
define
State after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Tactic:
obtain (c : Int) (h2 : a - b = m * c) from h1
State after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ ∃ c, b - a = ↑m * c
Tactic:
apply Exists.intro (-c)
State after:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = ↑m * -c

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = ↑m * -c
Tactic:
show b - a = m * (-c) from
  calc b - a
    _ = -(a - b) := by ring
    _ = -(m * c) := by rw [h2]
    _ = m * (-c) := by ring
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ b - a = -(a - b)
Tactic:
ring
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ -(a - b) = -(↑m * c)
Tactic:
rw [h2]
State after:
no goals

State before:
m : ℕ
a b : ℤ
h1 : ∃ c, a - b = ↑m * c
c : ℤ
h2 : a - b = ↑m * c
⊢ -(↑m * c) = ↑m * -c
Tactic:
ring
State after:
no goals