test: add test for issue fixed in previous commit

tests/lean/congrThmIssue.lean

@@ -0,0 +1,27 @@
+theorem Nat.lt_of_lt_le {x y z : Nat} : x < y → y ≤ z → x < z := by
+  intro h h'
+  induction h'
+  assumption
+  apply Nat.le_step
+  assumption
+
+structure ArrayBuffer (α) where
+  cap : Nat
+  backing : Fin cap → Option α
+  size : Nat
+  h_size : size ≤ cap
+  h_full : ∀ i, (h:i < size) → (backing ⟨i, Nat.lt_of_lt_le h h_size⟩).isSome
+
+namespace ArrayBuffer
+
+def grow : ArrayBuffer α → ArrayBuffer α :=
+λ ⟨cap, backing, size, h_size, h_full⟩ =>
+  ⟨cap + cap,
+    λ i => if h:i < cap then backing ⟨i,h⟩ else none,
+    size,
+    Nat.le_trans h_size (Nat.le_add_left _ _),
+    by intro i h
+       simp
+       trace_state
+       have : i < cap := Nat.lt_of_lt_le h h_size
+       simp [*]⟩

tests/lean/congrThmIssue.lean.expected.out

@@ -0,0 +1,10 @@
+α : Type ?u
+x✝ : ArrayBuffer α
+cap : Nat
+backing : Fin cap → Option α
+size : Nat
+h_size : size ≤ cap
+h_full : ∀ (i : Nat), i < size → Option.isSome (backing { val := i, isLt := (_ : i < cap) }) = true
+i : Nat
+h : i < size
+⊢ Option.isSome (if h : i < cap then backing { val := i, isLt := h } else none) = true