Theorem: near_mods (FormalSnarksProject/ToMathlib/ForTransformations.lean)

State before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
⊢ c = 0
Tactic:
have h := congr_arg (fun p => p % (d : ℤ)) habcd
State after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : (fun p => p % ↑d) ↑a = (fun p => p % ↑d) (↑b + c * ↑d)
⊢ c = 0

State before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : (fun p => p % ↑d) ↑a = (fun p => p % ↑d) (↑b + c * ↑d)
⊢ c = 0
Tactic:
simp_rw [Int.add_mul_emod_self, mod_cast_eq_cast_mod, Int.ofNat_inj] at h
State after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a % d = b % d
⊢ c = 0

State before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a % d = b % d
⊢ c = 0
Tactic:
simp only [ha, Nat.mod_eq_of_lt, hb] at h
State after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a = b
⊢ c = 0

State before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : ↑a = ↑b + c * ↑d
h : a = b
⊢ c = 0
Tactic:
rw [h, self_eq_add_right, mul_eq_zero, Nat.cast_eq_zero] at habcd
State after:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : c = 0 ∨ d = 0
h : a = b
⊢ c = 0

State before:
F : Type
inst✝ : Field F
a b d : ℕ
c : ℤ
ha : a < d
hb : b < d
habcd : c = 0 ∨ d = 0
h : a = b
⊢ c = 0
Tactic:
cases habcd <;> linarith
State after:
no goals