-- Mathlib/Algebra/Order/Floor.lean
theorem fract_mul_nat (a : α) (b : ℕ) : ∃ z : ℤ, fract a * b - fract (a * b) = z

Proof state:
case succ.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Tactic:
use z - y

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) = ↑(z - y)

Tactic:
rw [Int.cast_sub, ← hz, ← hy]

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ fract a * ↑0 - fract (a * ↑0) = ↑0

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
hc : ∃ z, fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Tactic:
rcases hc with ⟨z, hz⟩

Result:
case succ.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
b : ℕ
⊢ ∃ z, fract a * ↑b - fract (a * ↑b) = ↑z

Tactic:
induction' b with c hc

Result:
case zero
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ∃ z, fract a * ↑0 - fract (a * ↑0) = ↑z

case succ
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
hc : ∃ z, fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Proof state:
case zero
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ∃ z, fract a * ↑0 - fract (a * ↑0) = ↑z

Tactic:
use 0

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ fract a * ↑0 - fract (a * ↑0) = ↑0

Proof state:
case succ.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Tactic:
rcases fract_add (a * c) a with ⟨y, hy⟩

Result:
case succ.intro.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
y : ℤ
hy : fract (a * ↑c + a) - fract (a * ↑c) - fract a = ↑y
⊢ fract a * ↑c + fract a - fract (a * ↑c + a) =
    fract a * ↑c - fract (a * ↑c) - (fract (a * ↑c + a) - fract (a * ↑c) - fract a)

Tactic:
abel

Result:
no goals

Proof state:
case succ.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑(c + 1) - fract (a * ↑(c + 1)) = ↑z

Tactic:
rw [Nat.cast_add, mul_add, mul_add, Nat.cast_one, mul_one, mul_one]

Result:
case succ.intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
c : ℕ
z : ℤ
hz : fract a * ↑c - fract (a * ↑c) = ↑z
⊢ ∃ z, fract a * ↑c + fract a - fract (a * ↑c + a) = ↑z