From 490c75f8b5bb95ef4e7380feb19d767e7dfe9663 Mon Sep 17 00:00:00 2001
From: Chris Hughes <chrishughes24@gmail.com>
Date: Mon, 1 Apr 2019 19:32:43 +0100
Subject: [PATCH] tests

---
 src/data/padics/hensel.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/data/padics/hensel.lean b/src/data/padics/hensel.lean
index 73606387ee613..c5d6dd815028c 100644
--- a/src/data/padics/hensel.lean
+++ b/src/data/padics/hensel.lean
@@ -416,3 +416,5 @@ lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.deriv
 if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else
 by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _, soln_unique _ _⟩;
    assumption
+
+lemma aghk : true := trivial