diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out
index 231a213bb..ce21a1141 100644
--- a/tests/lean/tactic2.lean.expected.out
+++ b/tests/lean/tactic2.lean.expected.out
@@ -10,9 +10,4 @@ Theorem T2 : p ⇒ q ⇒ p ∧ q ∧ p := Discharge (λ H : p, Discharge (λ H::
 Theorem T3 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
     Discharge
         (λ H : p,
-           Discharge
-               (λ H::1 : p ∧ q,
-                  Discharge
-                      (λ H::2 : r,
-                         Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
-                              (Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))
+           Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))
diff --git a/tests/lean/tactic3.lean.expected.out b/tests/lean/tactic3.lean.expected.out
index 0c84eca2a..8536b12cd 100644
--- a/tests/lean/tactic3.lean.expected.out
+++ b/tests/lean/tactic3.lean.expected.out
@@ -7,9 +7,4 @@
 Theorem T1 : p ⇒ p ∧ q ⇒ r ⇒ q ∧ r ∧ p :=
     Discharge
         (λ H : p,
-           Discharge
-               (λ H::1 : p ∧ q,
-                  Discharge
-                      (λ H::2 : r,
-                         Conj (let H::1::2 := Conjunct2 H::1 in H::1::2)
-                              (Conj H::2 (let H::1::1 := Conjunct1 H::1 in H::1::1)))))
+           Discharge (λ H::1 : p ∧ q, Discharge (λ H::2 : r, Conj (Conjunct2 H::1) (Conj H::2 (Conjunct1 H::1)))))