case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)

case inr
m n : ℕ
h : n > 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
m n : ℕ
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
cases' Nat.eq_zero_or_pos n with h h
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
case inr
m n : ℕ
h : n > 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
replace h := Nat.succ_pred_eq_of_pos h
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + 1))
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
rw [← h, succ_eq_add_one]
no goals
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + 1))
calc
  gcd (fib m) (fib (n.pred + 1 + m)) =
      gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) := by
      rw [← fib_add n.pred _]
      ring_nf
  _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by
      rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
  _ = gcd (fib m) (fib (n.pred + 1)) :=
    coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (coprime.symm (fib_coprime_fib_succ m))
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (0 + m)) = gcd (fib m) (fib 0)
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
rw [h]
no goals
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (0 + m)) = gcd (fib m) (fib 0)
simp
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + m + 1))
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1))
rw [← fib_add n.pred _]
no goals
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + m + 1))
ring_nf
no goals
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1)) = gcd (fib m) (fib (pred n + 1) * fib (m + 1))
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]