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

State before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
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 c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
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 c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
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] at h
State after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
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 c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ c = 0
Tactic:
rw [emod_eq_of_lt ha', emod_eq_of_lt hb'] at h
State after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d

State before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
simp [h] at *
State after:
F : Type
inst✝ : Field F
a b c d : ℤ
hb' : 0 ≤ b
hb : b < d
ha' : 0 ≤ b
ha : b < d
habcd : c = 0 ∨ d = 0
h : True
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d

State before:
F : Type
inst✝ : Field F
a b c d : ℤ
hb' : 0 ≤ b
hb : b < d
ha' : 0 ≤ b
ha : b < d
habcd : c = 0 ∨ d = 0
h : True
⊢ c = 0

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
cases habcd <;> linarith
State after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d

State before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a = b % d
⊢ b < d

F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
exact hb
State after:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d

State before:
F : Type
inst✝ : Field F
a b c d : ℤ
ha' : 0 ≤ a
hb' : 0 ≤ b
ha : a < d
hb : b < d
habcd : a = b + c * d
h : a % d = b % d
⊢ a < d
Tactic:
exact ha
State after:
no goals